| products/Sources/formale Sprachen/Coq/man/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: branch Sprache: Unknown
|
Spracherkennung für: .1 vermutete Sprache: Fortran {Fortran[91] Abap[150] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen] .TH COQ 1 "October 11, 2006" .SH NAME coqtop \- The Coq Proof Assistant toplevel system .SH SYNOPSIS .B coqtop [ .B options ] .SH DESCRIPTION .B coqtop is the toplevel system of Coq, for interactive use. It reads phrases on the standard input, and prints results on the standard output. For batch-oriented use of Coq, see .BR coqc(1). .SH OPTIONS .TP .B \-h, \-\-help Help. Will give you the complete list of options accepted by coqtop. .TP .BI \-I \ dir, \ \-\-include \ dir add directory .I dir in the include path .TP .BI \-R \ dir\ coqdir recursively map physical .I dir to logical .I coqdir .TP .BI \-top \ coqdir set the toplevel name to be .I coqdir instead of Top .TP .B \-nois start with an empty initial state .TP .BI \-load\-ml\-object \ filename load ML object file .I filenname .TP .BI \-load\-ml\-source \ filename load ML file .I filename .TP .BI \-load\-vernac\-source \ filename, \ \-l \ filename load Coq file .I filename.v (Load filename.) .TP .BI \-load\-vernac\-source\-verbose \ filename, \ \-lv \ filename load verbosely Coq file .I filename.v (Load Verbose filename.) .TP .BI \-load\-vernac\-object \ path load Coq library .I path (Require path.) .TP .BI \-require \ path load Coq library .I path and import it (Require Import path.) .TP .B \-where print Coq's standard library location and exit .TP .B \-v print Coq version and exit .TP .B \-q skip loading of rcfile (resource file) if any .TP .BI \-init\-file \ filename set the rcfile to .I filename .TP .B \-batch batch mode (exits just after arguments parsing) .TP .B \-emacs tells Coq it is executed under Emacs .TP .BI \-dump\-glob \ filename dump globalizations in file f (to be used by .B coqdoc(1) ) .TP .B \-impredicative\-set set sort Set impredicative .TP .B \-dont\-load\-proofs don't load opaque proofs in memory .SH SEE ALSO .BR coqc (1), .BR coq-tex (1), .BR coqdep (1). .br .I The Coq Reference Manual. .I The Coq web site: http://coq.inria.fr [ Dauer der Verarbeitung: 0.106 Sekunden ] |