coq

Fragen
Coq ist ein formales Proof-Management-System und semi-interaktiver Theorembeweiser. Coq wird für die Zertifizierung von Programmiersprachenzertifizierungen, die Formalisierung von mathematischen Theoremen, das Lehren und mehr verwendet. Aufgrund des interaktiven Charakters von Coq empfehlen wir Ihnen, Fragen zu ausführbaren Beispielen unter https://x80.org/collacoq/ zu stellen, wenn dies angemessen erscheint.
2
Antworten

Berechne mit einer rekursiven Funktion, die durch eine wohldefinierte Induktion definiert ist

Wenn ich Function verwende, um eine nicht-strukturell rekursive Funktion in Coq zu definieren, verhält sich das resultierende Objekt merkwürdig, wenn eine bestimmte Berechnung angefordert wird. Anstatt das Ergebnis direkt anzugeben, gibt die...
02.09.2015, 13:16
1
Antwort

Beispiel für eine finite Karte

Für meine Anwendung muss ich die endlichen Karten in Coq verwenden und begründen. Um mich herum zu finden, habe ich über FMapAVL gefunden, das perfekt zu meinen Bedürfnissen passt. Das Problem ist, dass die Dokumentation knapp ist, und ich habe...
23.01.2013, 20:57
0
Antworten

Wie extrahiere ich das zweite Element von Sigma am Konstrukt Kalkül?

Ich versuche das folgendermaßen zu tun: %Vor% Beachten Sie, dass der Wert, der von dieser Funktion zurückgegeben wird, von einem Wert innerhalb des Sigma selbst abhängt, ich diesen Wert extrahieren muss. Dieser Code überprüft nicht, weil ich...
13.05.2017, 20:15
2
Antworten

Wie wird der Parser von Coq implementiert?

Ich war völlig erstaunt, wie Coqs Parser implementiert ist. z.B. Ссылка Es ist so verrückt, dass der Parser in Ordnung scheint, ein Lexem zu nehmen, indem er einen Notationsbefehl gibt, und der nachfolgende Parser ist in der Lage, jeden...
03.04.2017, 12:26