coqtop - Online sa Cloud

PROGRAMA:

NAME

coqtop - Ang Coq Proof Assistant toplevel system

SINOPSIS

coqtop [ pagpipilian ]

DESCRIPTION

coqtop ay ang toplevel system ng Coq, para sa interactive na paggamit. Nagbabasa ito ng mga parirala sa
karaniwang input, at nagpi-print ng mga resulta sa karaniwang output.

Para sa batch-oriented na paggamit ng Coq, tingnan coqcNa (1).

Opsyon

-h, - Tumulong
Tulong. Bibigyan ka ng kumpletong listahan ng mga opsyon na tinanggap ng coqtop.

-I ay, --isama dir
magdagdag ng direktoryo dir sa isamang landas

-R dir coqdir
recursively mapa pisikal dir sa lohikal coqdir

-tuktok coqdir
itakda ang toplevel na pangalan upang maging coqdir sa halip na Top

-inputstate filename, -ay filename
basahin ang estado mula sa file filename.coq

- ingay magsimula sa isang walang laman na paunang estado

-outputstatefilename
isulat ang estado sa file filename.coq

-load-ml-object filename
i-load ang ML object file filenname

-load-ml-source filename
i-load ang ML file filename

-load-vernac-source filename, -l filename
i-load ang Coq file filename.v (I-load ang filename.)

-load-vernac-source-verbose filename, -lv filename
mag-load ng verbosely Coq file filename.v (I-load ang Verbose filename.)

-load-vernac-object filename
i-load ang Coq object file filename.vo

-kailangan filename
i-load ang Coq object file filename.vo at i-import ito (Kailangan ang Import filename.)

-compile filename
i-compile ang Coq file filename.v (nagpapahiwatig -batch )

-compile-verbose filename
verbosely compile Coq file filename.v (nagpapahiwatig -batch )

-optino patakbuhin ang native-code na bersyon ng Coq

-byte patakbuhin ang bytecode na bersyon ng Coq

-saan i-print ang karaniwang lokasyon at labasan ng library ng Coq

-v i-print ang bersyon ng Coq at lumabas

-q laktawan ang paglo-load ng rcfile

-init-file filename
itakda ang rcfile sa filename

-batch batch mode (lumalabas pagkatapos ng pag-parse ng mga argumento)

-boot boot mode (nagpapahiwatig -q at -batch )

-emacs nagsasabi sa Coq na ito ay isinasagawa sa ilalim ng Emacs

-dump-glob filename
itapon ang mga globalisasyon sa file f (gamitin ng coqdoc(1) )

-may-geoproof (oo|hindi)
upang (i-de)isaaktibo ang mga espesyal na function para sa Geoproof sa loob ng Coqide (default ay oo )

-impredicative-set
set sort Itakda impredicative

-dont-load-proofs
huwag mag-load ng opaque proofs sa memorya

-xml i-export ang mga XML file alinman sa hierarchy na naka-root sa direktoryo
$COQ_XML_LIBRARY_ROOT (kung nakatakda) o sa stdout (kung hindi nakatakda)

-Kalidad
pagbutihin ang pagiging madaling mabasa ng mga tuntunin ng patunay na ginawa ng ilang taktika

Gumamit ng coqtop online gamit ang mga serbisyo ng onworks.net