Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
NatPlus fehlt und Frage zu views
Bei mir gibt es nicht die theory NatPlus. Ich habe es mit der von der Website probiert (unter “Formalisierungen des letzten Kurses”) aber das geht komplett kaputt. Außerdem wird mein AbelianMonoid auch als Fehler in dem view (also in dem Teil der den Typ des NatIsMonoid angibt (“?AbelianMonoid → ?NatPlus”)). Der Fehler ist “unknown identifier” . Der AbelianMonoid ist aber Fehlerfrei (also ohne Fehlermeldungen).
Dann noch eine Frage zur opposite Group (bzw auch zu views allgemein): wenn ich den View zu opposite group erstelle, dann kann ich ja nur mappings für axiome angeben und nicht für Theoreme. Das Problem ist nun , dass ich left_inverse_axiom nicht angeben kann. Allerdings kann ich das auch nicht als Theorem schreiben (mit sketch). Darum auch die Frage, kann man views mit Theoremen erweitern (und wenn ja, dann wie ?). Und wie verwendet man views in anderen Theories (beim includen bekomme ich einen Fehler)?
Und dann noch eine abschließende Frage : kann ich das ganze irgendwie testen ? Wie würde z.B. ein Beweis von a + b = b + a in einer Gruppe aussehen (ja ist trivial , will aber nur wissen , wie man das MMT beibringt)?
Sorry für die vielen Fragen und danke im Voraus.
Ich hab die aktuelle Numbers.mmt gerade bei studon hochgeladen, ist jetzt also vorhanden 
Wenn NatPlus nicht existiert ist das natürlich kein Wunder 
mit sketch kannst du eigentlich alles angeben… Ein theorem ist ein Beweisterm vom type |- P für irgendeine Proposition P. „sketch „bla““ hat immer den typ |- P für jede proposition, da sollte eigentlich nichts schief gehen können. Falls doch erläuter mir nochmal die Situation genauer, vielleicht seh ich dann was warum schief läuft
Naja, mathematisch gesehen existiert so ein Beweis erstmal nicht, weil Gruppen ja nicht kommutativ sein müssen. MMT ist das aber natürlich egal, mit sketch kannst du also trotzdem einen Beweis liefern.
Wie ein formal korrekter Beweis aussähe (wenn es einen gäbe): Er bestünde halt (in unserem Fall) aus den Natural Deduction proof rules die wir/ihr derzeit formalisiert