coqtop - Online nel cloud

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 ed -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