coqtop - Online în cloud

PROGRAM:

NUME

coqtop - Sistemul de nivel superior Coq Proof Assistant

REZUMAT

coqtop [ Opțiuni ]

DESCRIERE

coqtop este sistemul de nivel superior al Coq, pentru utilizare interactivă. Citește fraze pe
intrare standard și imprimă rezultatele pe rezultatul standard.

Pentru utilizarea Coq orientată pe loturi, vezi coqc(1).

OPŢIUNI

-h, --Ajutor
Ajutor. Vă va oferi lista completă a opțiunilor acceptate de coqtop.

-I este, --include dir
adaugă directorul dir în calea include

-R dir coqdir
mapează recursiv fizic dir la logic coqdir

-top coqdir
setați numele de nivel superior să fie coqdir în loc de Top

-stare de intrare nume de fișier, -este nume de fișier
Citiți starea din fișier nume de fișier.coq

-nu este începe cu o stare inițială goală

-stare ieșirenume de fișier
starea de scriere în fișier nume de fișier.coq

-load-ml-obiect nume de fișier
încărcați fișierul obiect ML nume de fișier

-load-ml-source nume de fișier
încărcați fișierul ML nume de fișier

-load-vernac-source nume de fișier, -l nume de fișier
încărcați fișierul Coq nume de fișier.v (Încărcați numele fișierului.)

-load-vernac-source-verbose nume de fișier, -lv nume de fișier
încărcați în mod pronunțat fișierul Coq nume de fișier.v (Încărcați numele fișierului Verbose.)

-încărcare-obiect-vernac nume de fișier
încărcați fișierul obiect Coq nume de fișier.vo

-cere nume de fișier
încărcați fișierul obiect Coq nume de fișier.vo și importați-l (Necesită importarea numelui fișierului.)

-compila nume de fișier
compilați fișierul Coq nume de fișier.v (implică -lot )

-compilare-verbosă nume de fișier
compilați cu atenție fișierul Coq nume de fișier.v (implică -lot )

-opta rulați versiunea de cod nativ a Coq

-octet rulați versiunea bytecode a Coq

-Unde imprimați locația standard a bibliotecii Coq și ieșiți

-v tipăriți versiunea Coq și ieșiți

-q omite încărcarea fișierului rc

-init-file nume de fișier
setați fișierul rc la nume de fișier

-lot modul lot (iese imediat după analizarea argumentelor)

- cizma modul de pornire (implică -q si -lot )

-emacs îi spune lui Coq că este executat sub Emacs

-dump-glob nume de fișier
aruncați globalizările în fișierul f (pentru a fi folosit de coqdoc(1) )

-cu-geoproof (da|nu)
pentru a (dez)activa funcții speciale pentru Geoproof în Coqide (implicit este da )

-impredicative-set
set sort Set impredicativ

-dont-load-proofs
nu încărcați dovezi opace în memorie

-xml exportați fișiere XML fie în ierarhia înrădăcinată în director
$COQ_XML_LIBRARY_ROOT (dacă este setat) sau la stdout (dacă este nesetat)

-Calitate
îmbunătățește lizibilitatea termenilor de probă produse de unele tactici

Utilizați coqtop online folosind serviciile onworks.net