8 votes
Accepted

Are eliminators useful in practice, or are they only useful in the metatheory?

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 ...
Andrej Bauer's user avatar
  • 8,969
5 votes
Accepted

Explain all the arguments to this rec eliminator

I found hints of the answer here The original definition of JSON "falls outside the strict specification of an inductive type" because ...
Felipe's user avatar
  • 273
3 votes
Accepted

What is an eliminator?

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 ...
Couchy's user avatar
  • 2,211
2 votes
Accepted

Coq's elimination restriction corner cases -- when can you eliminate Prop's into Type?

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 ...
Meven Lennon-Bertrand's user avatar
2 votes

Are eliminators useful in practice, or are they only useful in the metatheory?

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 ...
Molly Stewart-Gallus's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible