To jest polecenie coqtop, które można uruchomić u dostawcy bezpłatnego hostingu OnWorks przy użyciu jednej z naszych wielu bezpłatnych stacji roboczych online, takich jak Ubuntu Online, Fedora Online, emulator online systemu Windows lub emulator online systemu MAC OS
PROGRAM:
IMIĘ
coqtop - system Coq Proof Assistant na najwyższym poziomie
STRESZCZENIE
koktop [ Opcje ]
OPIS
koktop to najwyższy poziom systemu Coq do użytku interaktywnego. Czyta wyrażenia na
standardowe wejście i wypisuje wyniki na standardowe wyjście.
Informacje na temat zastosowania Coq w trybie wsadowym można znaleźć w artykule kok(1).
OPCJE
-H, --help
Pomoc. Wyświetli pełną listę opcji akceptowanych przez coqtop.
-I reż, --włączać reż
dodaj katalog reż w ścieżce dołączania
-R reż koqdir
rekursywnie mapować fizyczne reż do logicznego koqdir
-Top koqdir
ustaw nazwę najwyższego poziomu na koqdir zamiast góry
-stan wejściowy Nazwa pliku, -jest filename
odczytaj stan z pliku nazwapliku.coq
- hałas zacznij od pustego stanu początkowego
-stan wyjściowyfilename
zapisz stan w pliku nazwapliku.coq
-load-ml-obiekt filename
załaduj plik obiektowy ML nazwapliku
-ładuj-ml-źródło filename
załaduj plik ML filename
-load-vernac-source Nazwa pliku, -l filename
załaduj plik Coq nazwapliku.v (Wczytaj nazwę pliku.)
-load-vernac-source-verbose Nazwa pliku, -poz filename
załaduj szczegółowy plik Coq nazwapliku.v (Załaduj pełną nazwę pliku.)
-load-vernac-obiekt filename
załaduj plik obiektowy Coq nazwapliku.vo
-wymagać filename
załaduj plik obiektowy Coq nazwapliku.vo i zaimportuj go (Wymagaj importu nazwy pliku.)
-skompilować filename
skompiluj plik Coq nazwapliku.v (implikuje -seria )
-kompilacja-pełna filename
szczegółowo skompiluj plik Coq nazwapliku.v (implikuje -seria )
-optować uruchom wersję Coq z natywnym kodem
-bajt uruchom wersję Coq w kodzie bajtowym
-gdzie wydrukuj standardową lokalizację biblioteki Coq i wyjdź
-v wydrukuj wersję Coq i wyjdź
-q pomiń ładowanie pliku rc
-plik-inicjujący filename
ustaw plik rc na filename
-seria tryb wsadowy (wychodzi zaraz po przeanalizowaniu argumentów)
-bagażnik tryb rozruchu (co oznacza -q i -seria )
-emaks mówi Coqowi, że jest wykonywany w Emacsie
-dump-glob filename
zrzuć globalizacje w pliku f (do użycia przez koqdoc(1) )
-z-geoodpornym (tak|nie)
aby (de)aktywować specjalne funkcje Geoproof w Coqide (domyślnie jest to tak )
-zestaw imperatywny
ustaw sortowanie Ustaw imperdykat
-Dont-load-proofs
nie ładuj nieprzezroczystych wydruków próbnych do pamięci
-xml eksportuj pliki XML do hierarchii znajdującej się w katalogu
$COQ_XML_LIBRARY_ROOT (jeśli ustawione) lub na standardowe wyjście (jeśli nieustawione)
Jakości
poprawić czytelność warunków dowodowych generowanych przez niektóre taktyki
Korzystaj z coqtop online, korzystając z usług onworks.net
