coqtop - Online in de cloud

PROGRAMMA:

NAAM

coqtop - Het Coq Proof Assistant toplevelsysteem

KORTE INHOUD

koktop [ opties ]

PRODUCTBESCHRIJVING

koktop is het toplevelsysteem van Coq, voor interactief gebruik. Het leest zinnen op de
standaardinvoer en drukt de resultaten af ​​op de standaarduitvoer.

Voor batchgericht gebruik van Coq, zie coqc(1).

OPTIES

-H, --help
Hulp. Geeft u de volledige lijst met opties die door coqtop worden geaccepteerd.

-I richt, --erbij betrekken dir
map toevoegen dir in het include-pad

-R dir coqdir
recursief fysiek in kaart brengen dir logisch coqdir

-bovenkant coqdir
stel de naam op het hoogste niveau in coqdir in plaats van Top

-invoerstatus bestandsnaam, -is bestandsnaam
status uit bestand lezen bestandsnaam.coq

-Nee is beginnen met een lege begintoestand

-uitvoerstatusbestandsnaam
schrijf status in bestand bestandsnaam.coq

-load-ml-object bestandsnaam
ML-objectbestand laden bestandsnaam

-load-ml-bron bestandsnaam
ML-bestand laden bestandsnaam

-laad-vernac-bron bestandsnaam, -l bestandsnaam
Coq-bestand laden bestandsnaam.v (Laad bestandsnaam.)

-load-vernac-source-uitgebreid bestandsnaam, -lv bestandsnaam
laad het Coq-bestand uitgebreid bestandsnaam.v (Laad uitgebreide bestandsnaam.)

-load-vernac-object bestandsnaam
laad het Coq-objectbestand bestandsnaam.vo

-vereisen bestandsnaam
laad het Coq-objectbestand bestandsnaam.vo en importeer het (vereist importbestandsnaam.)

-compileren bestandsnaam
Coq-bestand compileren bestandsnaam.v (impliceert -partij )

-compileer-uitgebreid bestandsnaam
compileer Coq-bestand uitvoerig bestandsnaam.v (impliceert -partij )

-opt voer de native-codeversie van Coq uit

-byte voer de bytecodeversie van Coq uit

-waar druk de standaardbibliotheeklocatie van Coq af en sluit af

-v druk de Coq-versie af en sluit af

-q sla het laden van rcfile over

-init-bestand bestandsnaam
stel het rcbestand in op bestandsnaam

-partij batchmodus (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 bestandsnaam
dump globalisaties in bestand f (te gebruiken door coqdoc(1) )

-met-geoproof (ja|nee)
om speciale functies voor Geoproof binnen Coqide te (de)activeren (standaard is ja )

-impredicatieve-set
set sort Stel impredicatief in

-dont-load-bewijzen
laad geen ondoorzichtige proefdrukken in het geheugen

-xml exporteer XML-bestanden naar de hiërarchie die in de map is geworteld
$COQ_XML_LIBRARY_ROOT (indien ingesteld) of naar stdout (indien niet ingesteld)

-Kwaliteit
de leesbaarheid verbeteren van de bewijstermen die door sommige tactieken worden geproduceerd

Gebruik coqtop online met behulp van onworks.net-services