Aceasta este comanda coqide.byte care poate fi rulată în furnizorul de găzduire gratuit OnWorks folosind una dintre multiplele noastre stații de lucru online gratuite, cum ar fi Ubuntu Online, Fedora Online, emulator online Windows sau emulator online MAC OS
PROGRAM:
NUME
coqide - Interfața grafică Coq Proof Assistant
REZUMAT
coqide [ Opțiuni ]
DESCRIERE
coqide este o interfață grafică gtk pentru asistentul Coq proof.
Pentru utilizarea Coq orientată către linia de comandă, consultați coqtop(1) ; pentru utilizarea Coq orientată pe loturi, vezi
coqc(1).
OPŢIUNI
-h Afișați lista completă de opțiuni acceptate de coqide.
-I dir, -include dir
Adăugați directorul director în calea include.
-R dir coqdir
Hartă fizică recursiv dir la logic coqdir.
-src Adăugați directoare sursă în calea include.
-este f, -stare de intrare f
Citiți starea de la f.coq.
-nu este Începeți cu o stare goală.
-stare ieșire f
Scrieți starea în fișier f.coq.
-load-ml-obiect f
Încărcați fișierul obiect ML f.
-load-ml-source f
Încărcați fișierul ML f.
-l f, -load-vernac-source f
Încărcați fișierul Coq f.v (Încărcare f.).
-lv f, -load-vernac-source-verbose f
Încărcați fișierul Coq f.v (Încărcare Verbose f.).
-încărcare-obiect-vernac f
Încărcați fișierul obiect Coq f.vo.
-cere f
Încărcați fișierul obiect Coq f.vo și importați-l (Necesită f.).
-compila f
Compilați fișierul Coq f.v (implică -lot).
-compilare-verbosă f
Compilați în mod verbal fișierul Coq f.v (implică -lot).
-opta Rulați versiunea de cod nativ a Coq sau Coq_SearchIsos.
-octet Rulați versiunea bytecode a Coq sau Coq_SearchIsos.
-Unde Tipăriți locația standard a bibliotecii Coq și ieșiți.
-v Imprimați versiunea Coq și ieșiți.
-q Omite încărcarea fișierului rc.
-init-file f
Setați fișierul rc la f.
-lot Modul lot (iese imediat după analizarea argumentelor).
- cizma Modul de pornire (implică -q și -lot).
-emacs Spune lui Coq că este executat sub Emacs.
-dump-glob f
Descarcă globalizările în fișier f (pentru a fi folosit de coqdoc(1)).
-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).
Utilizați coqide.byte online folosind serviciile onworks.net