Aceasta este comanda coqc 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
coqc - Compilatorul Coq Proof Assistant
REZUMAT
coqc [ general Cocoş Opțiuni ] fişier
DESCRIERE
coqc este compilatorul de loturi pentru Coq Proof Assistant. Opțiunile sunt practic cele
la fel ca coqtop(1). dosar.v este fișierul vernacular de compilat. fişier trebuie format numai
cu caracterele de la `a` la `Z`, `0`-`9` sau `_` și trebuie să înceapă cu o literă. The
compilatorul produce un fișier obiect fişier.vo.
Pentru utilizarea interactivă a Coq, vezi coqtop(1).
OPŢIUNI
coqc este un script care rulează pur și simplu coqtop cu optiune -compila acceptă aceleași opțiuni
as coqtop.
-imagine bin
utilizare bin ca subiacent coqtop în locul celui implicit.
-verbos
tipăriți fișierul compilat pe rezultatul standard.
Utilizați coqc online folosind serviciile onworks.net
