Questo è il comando coqtop che può essere eseguito nel provider di hosting gratuito OnWorks utilizzando una delle nostre molteplici workstation online gratuite come Ubuntu Online, Fedora Online, emulatore online Windows o emulatore online MAC OS
PROGRAMMA:
NOME
coqtop - Il sistema di primo livello Coq Proof Assistant
SINOSSI
coqtop [ Opzioni ]
DESCRIZIONE
coqtop è il sistema di primo livello di Coq, per uso interattivo. Legge frasi sul
input standard e stampa i risultati sull'output standard.
Per l'uso orientato ai batch di Coq, vedere coqc(1).
VERSIONI
-H, --Aiuto
Aiuto. Ti darà l'elenco completo delle opzioni accettate da coqtop.
-I dire, --includere dir
aggiungi directory dir nel percorso di inclusione
-R dir coqdir
mappare ricorsivamente fisica dir a logico coqdir
-superiore coqdir
imposta il nome di livello superiore su essere coqdir invece di Top
-stato di ingresso nome del file, -è Nome del file
leggi lo stato dal file nomefile.coq
-rumore inizia con uno stato iniziale vuoto
-stato di uscitaNome del file
scrivi lo stato nel file nomefile.coq
-load-ml-oggetto Nome del file
carica il file oggetto ML nomefile
-load-ml-sorgente Nome del file
carica il file ML Nome del file
-load-vernac-source nome del file, -l Nome del file
carica il file Coq nomefile.v (Carica il nome del file.)
-load-vernac-source-verbose nome del file, -liv Nome del file
caricare in modo dettagliato il file Coq nomefile.v (Carica nome file dettagliato.)
-load-vernac-oggetto Nome del file
carica il file oggetto Coq nomefile.vo
-richiedere Nome del file
carica il file oggetto Coq nomefile.vo e importalo (Richiedi nome file di importazione.)
-compilare Nome del file
compila il file Coq nomefile.v (implica -lotto )
-compilare-verbose Nome del file
compilare in modo dettagliato il file Coq nomefile.v (implica -lotto )
-optare eseguire la versione in codice nativo di Coq
-byte eseguire la versione bytecode di Coq
-dove stampa la posizione della libreria standard di Coq ed esci
-v stampa la versione Coq ed esci
-q salta il caricamento di rcfile
-file-init Nome del file
imposta il file rc su Nome del file
-lotto modalità batch (esce subito dopo l'analisi degli argomenti)
-stivale modalità di avvio (implica -q e a -lotto )
-emac dice a Coq che viene eseguito sotto Emacs
-glob di scarico Nome del file
scarica le globalizzazioni nel file f (da usare da coqdoc(1) )
-con-geoproof (sì|no)
per (dis)attivare funzioni speciali per Geoproof all'interno di Coqide (l'impostazione predefinita è sì )
-insieme-impredicativo
set sort Imposta impredicativo
-non-caricare-prove
non caricare prove opache in memoria
-xml esporta i file XML nella gerarchia radicata nella directory
$COQ_XML_LIBRARY_ROOT (se impostato) o su stdout (se non impostato)
Qualità
migliorare la leggibilità dei termini di prova prodotti da alcune tattiche
Usa coqtop online utilizzando i servizi onworks.net