Dit is de opdracht coqide die kan worden uitgevoerd in de gratis hostingprovider van OnWorks met behulp van een van onze meerdere gratis online werkstations zoals Ubuntu Online, Fedora Online, Windows online emulator of MAC OS online emulator
PROGRAMMA:
NAAM
coqide - De grafische interface van Coq Proof Assistant
KORTE INHOUD
coqide [ opties ]
PRODUCTBESCHRIJVING
coqide is een gtk grafische interface voor de Coq proof-assistent.
Voor opdrachtregelgericht gebruik van Coq, zie: koktop(1) ; voor batchgericht gebruik van Coq, zie
coqc(1).
OPTIES
-h Toon de volledige lijst met opties die zijn geaccepteerd door coqide.
-I dir, omvatten dir
Voeg directory dir toe aan het include-pad.
-R dir coqdir
Recursief fysiek in kaart brengen dir logisch coqdir.
-src Voeg bronmappen toe aan het include-pad.
-is f, -invoerstatus f
Status lezen van f.coq.
-Nee is Begin met een lege toestand.
-uitvoerstatus f
Schrijf staat in bestand f.coq.
-load-ml-object f
Laad ML-objectbestand f.
-load-ml-bron f
Laad ML-bestand f.
-l f, -laad-vernac-bron f
Laad Coq-bestand f.v (Laden f.).
-lv f, -load-vernac-source-uitgebreid f
Laad Coq-bestand f.v (Uitgebreid laden f.).
-load-vernac-object f
Laad Coq-objectbestand f.vo.
-vereisen f
Laad Coq-objectbestand f.vo en importeer het (vereist f.).
-compileren f
Coq-bestand compileren f.v (impliceert -partij).
-compileer-uitgebreid f
Coq-bestand uitgebreid compileren f.v (impliceert -partij).
-opt Voer de native-codeversie van Coq of Coq_SearchIsos uit.
-byte Voer de bytecode-versie van Coq of Coq_SearchIsos uit.
-waar Print de standaard bibliotheeklocatie van Coq en sluit af.
-v Coq-versie afdrukken en afsluiten.
-q Sla het laden van rcfile over.
-init-bestand f
Zet het rc-bestand op f.
-partij Batch-modus (wordt afgesloten net na het parseren van de argumenten).
-laars Opstartmodus (impliceert -q en -partij).
-emacs Vertelt Coq dat het wordt uitgevoerd onder Emacs.
-dump-glob f
Globaliseringen in bestand dumpen f (te gebruiken door coqdoc(1)).
-impredicatieve-set
Sorteer instellen Impredicatief instellen.
-dont-load-bewijzen
Laad geen ondoorzichtige bewijzen in het geheugen.
-xml Exporteer XML-bestanden naar de hiërarchie die in de directory is geworteld
COQ_XML_LIBRARY_ROOT (indien ingesteld) of naar stdout (indien uitgeschakeld).
Gebruik coqide online met onworks.net-services
