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.66Quellennavigators
]
