Chapter 13: ML-style pattern-matching
Cristina Cornes
This 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 ?
