Untersuchungsergebnis.rst Download desShell {Shell[87] Cobol[88] C[112]}zum Wurzelverzeichnis wechseln
==========================
Introduction and Contents
==========================
.. include:: introduction.rst
Contents
--------
.. toctree::
:caption: Indexes
genindex
coq-cmdindex
coq-tacindex
coq-optindex
coq-exnindex
.. No entries yet
* :index:`thmindex`
.. toctree::
:caption: Preamble
self
history
changes
.. toctree::
:caption: The language
language/gallina-specification-language
language/gallina-extensions
language/coq-library
language/cic
language/module-system
.. toctree::
:caption: The proof engine
proof-engine/vernacular-commands
proof-engine/proof-handling
proof-engine/tactics
proof-engine/ltac
proof-engine/detailed-tactic-examples
proof-engine/ssreflect-proof-language
.. toctree::
:caption: User extensions
user-extensions/syntax-extensions
user-extensions/proof-schemes
.. toctree::
:caption: Practical tools
practical-tools/coq-commands
practical-tools/utilities
practical-tools/coqide
.. toctree::
:caption: Addendum
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::
:caption: Reference
zebibliography
.. 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).
[ zur Elbe Produktseite wechseln0.69Quellennavigators
]
