Proof checking
Recursor
The elimination rule used to define functions or proofs by cases on an inductive value.
Definition
Recursor
A recursor describes how to consume every constructor of an inductive type.
For natural numbers, a recursor takes a zero case and a successor step. Induction is the dependent form in which the result type may vary with the number.
01
Example
Addition can recurse on its second natural-number argument with a zero case and a successor case.
02
Important distinction
A recursor must follow the rules generated for its specific inductive declaration.
After reading this article, you should be able to
- Define Recursor in the sense used on this site.
- Match each constructor of an inductive type to the case required by its recursor.