| products/Sources/formale Sprachen/Coq/doc/sphinx/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: Tactics.v Sprache: Coq
|
Untersuchungsergebnis.rst Download desAda {Ada[141] Abap[356] [0]}zum Wurzelverzeichnis wechseln ========================== The Coq Reference Manual ========================== ------------ Introduction ------------ .. include:: introduction.rst .. include:: license.rst .. [#PG] Proof-General is available at https://proofgeneral.github.io/. Optionally, you can enhance it with the minor mode Company-Coq :cite:`Pit16` (see https://github.com/cpitclaudel/company-coq). .. include:: history.rst .. include:: changes.rst ------------ The language ------------ .. toctree:: language/gallina-specification-language language/gallina-extensions language/coq-library language/cic language/module-system ---------------- The proof engine ---------------- .. toctree:: proof-engine/vernacular-commands proof-engine/proof-handling proof-engine/tactics proof-engine/ltac proof-engine/detailed-tactic-examples proof-engine/ssreflect-proof-language --------------- User extensions --------------- .. toctree:: user-extensions/syntax-extensions user-extensions/proof-schemes --------------- Practical tools --------------- .. toctree:: practical-tools/coq-commands practical-tools/utilities practical-tools/coqide -------- Addendum -------- .. toctree:: addendum/extended-pattern-matching addendum/implicit-coercions addendum/canonical-structures addendum/type-classes addendum/omega addendum/micromega addendum/extraction addendum/program addendum/ring addendum/nsatz addendum/generalized-rewriting addendum/parallel-proof-processing addendum/miscellaneous-extensions addendum/universe-polymorphism addendum/sprop .. toctree:: zebibliography [ zur Elbe Produktseite wechseln0.176Quellennavigators ] |