Coq Fehler: Die Referenz evenb wurde nicht in der aktuellen Umgebung gefunden

Ich versuche, durch die Software Foundations Coq Buch (http://www.cis.upenn.edu/~bcpierce/sf/current/toc.html) gehen, aber wenn ich Induction.v kompilieren (die wie http://www.cs.uml.edu/~rhenniga/coq/sf_induction.html aussieht), bekomme ich den Fehler Meldung "Fehler: Die Referenz Evenb wurde in der aktuellen Umgebung nicht gefunden." - auch nach der Kompilation von Basics.v. Irgendwelche Ideen warum?Coq Fehler: Die Referenz evenb wurde nicht in der aktuellen Umgebung gefunden

Quelle

2016-04-03 user2908789

Wir brauchen etwas mehr Kontext zu wissen, was falsch sein könnte. Verwenden Sie CoqIDE? Ist Basics.v im selben Verzeichnis wie Induction.v? Wird die kompilierte Datei Basics.vo tatsächlich in diesem Verzeichnis angezeigt? –

Versuchen Sie, 'LoadPath hinzufügen '." 'Am Anfang von' Induction.v' gemäß [dieser Antwort] hinzuzufügen (http://stackoverflow.com/a/16203673/596361). –

Kompilieren Basic.v mit coqc Basics.v Befehl sollte Basic.vo und Basic.glob Dateien im selben Verzeichnis erstellen. Dann sollten Sie auch Induction.v im gleichen Verzeichnis kompilieren; coqc Induction.v.

Quelle

2016-04-15 20:54:12

I can confirm that opening CoqIDE from the same directory works on macOS: cd <sf-dir>; /Applications/CoqIDE_8.5.app/Contents/MacOS/coqide

aus: The reference "X" was not found in the current environment

Quelle

2017-06-09 10:55:16

Coq Fehler: Die Referenz evenb wurde nicht in der aktuellen Umgebung gefunden

Antwort

Verwandte Themen