Chapter 13: ML-style pattern-matching
Cristina CornesThis section describes the full form of pattern-matching in Coq terms.
The current implementation contains two strategies, one for compiling non-dependent case and another one for dependent case.
- 13.1 Patterns
- 13.2 About patterns of parametric types
- 13.3 Matching objects of dependent types
- 13.4 Using pattern matching to write proofs
- 13.5 When does the expansion strategy fail ?