Coq
8.7
The language
The Gallina specification language
Extensions of Gallina
The Coq library
Calculus of Inductive Constructions
The Module System
The proof engine
Vernacular commands
Proof handling
Tactics
The tactic language
Detailed examples of tactics
The SSReflect proof language
User extensions
Syntax extensions and interpretation scopes
Proof schemes
Practical tools
The Coq commands
Utilities
Coq Integrated Development Environment
Addendum
Extended pattern-matching (full text)
Implicit Coercions
Canonical Structures
Type Classes
Omega: a solver for quantifier-free problems in Presburger Arithmetic
Micromega: tactics for solving arithmetic goals over ordered rings
Extraction of programs in Objective Caml and Haskell
Program
The ring and field tactic families
Nsatz: tactics for proving equalities in integral domains
Generalized rewriting
Asynchronous and Parallel Proof Processing
Polymorphic Universes
Miscellaneous extensions
Coq glossary
Porting to Sphinx
The Gallina specification language
Calculus of Inductive Constructions
A subset of Coq's tactic reference
A few examples of trickier syntax constructs
Coq
Docs
»
Canonical Structures
View page source
Canonical Structures
¶
Source:
https://coq.inria.fr/distrib/current/refman/canonical-structures.html
Converted by:
Maxime Dénès