Chapter 2: Extensions of Gallina
Gallina is the kernel language of Coq. We describe here extensions of the Gallina's syntax.- 2.1 Record types
- 2.2 Variants and extensions of Cases
- 2.3 Forced type
- 2.4 Local definitions
- 2.5 Section mechanism
- 2.6 Implicit arguments
- 2.7 Implicit Coercions