Jestem nowicjuszem Coq i dlatego chcę lepiej zrozumieć sprawdzanie dowodów Próbuję użyć biblioteki Ssreflect.Błąd ścieżki ładowania CoqIDE dla ssreflect
Zainstalowałem Ssreflect v 1.5 na Mac OS v 10.10.3 (Yosemite), który działa w Terminalu.
Jednak gdy próbowałem załadować biblioteki w CoqIDE 8.4p15 używając:
Require Import ssreflect.
pojawia się błąd:
Cannot find library ssreflect in loadpath
Próbowałem, używając:
Add LoadPath "/opt/local/lib/coq/user-contrib/Ssreflect/".
gdzie SSRCOQ_LIB jest aktualnie ustawiony, ale pojawia się błąd:
The file /opt/local/lib/coq/user-contrib/Ssreflect/ssreflect.vo contains library Ssreflect.ssreflect and not library ssreflect
Wdzięczny za pomoc w załadowaniu biblioteki ssreflect z poziomu CoqIDE.
yay! Dziękujemy za publikację. Utknąłem na tym na zawsze. W przypadku homebrew możesz wykonać te same instrukcje, ale użyj "coqtop" homebrew: 'coqtop' ->'/usr/local/bin/coqtop', wklej to! –