Tag Info

Indeed, there are parallels between definitions by pattern matching and eliminators. A typical eliminator is just a shallow pattern. For example, the simple recursor for natural numbers can be defined ...

I found hints of the answer here The original definition of JSON "falls outside the strict specification of an inductive type" because ...

The role of constructors and eliminators can be understood through category theory. For every type former (for example $A\times B$, $A+B$, $A^B$, $\mathbb N$, etc...) we can ask How can we construct ...

First, let me answer your last question: as far as I know, the reference manual calls the restriction "empty or singleton elimination", I have seen "subsingleton elimination" or ...

One practical use of induction principles is the Scott encoding of datatypes. This isn't so useful directly in theorem proving because useful use of Scott encoded datatypes usually requires some form ...