Questions tagged [eliminator]

eliminators are proof relevant eliminations.

Filter by
Sorted by
Tagged with
3 votes
1 answer
96 views

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

In order to ensure soundness, and to keep axioms like proof irrelevance admissible, Coq has an "elimination restriction" on inductive types in Prop. ...
JoJoModding's user avatar
5 votes
1 answer
139 views

Explain all the arguments to this rec eliminator

I defined this inductive type for representing JSON elements ...
Felipe's user avatar
  • 273
3 votes
0 answers
122 views

Uniform notions of pattern matching at dependent types with impredicative proof strength

I am looking for axioms/inference rules that satisfy the following 3 conditions: can be added to predicative intensional Martin-Löf type theory, so $\Pi$, $\Sigma$, equality type, with W-types, ...
Ilk's user avatar
  • 517
3 votes
1 answer
179 views

What is an eliminator?

What is an eliminator? Are there any differences between an eliminator and an elimination form (such as $\pi_1$ and $\pi_2$ for binary products)? Does every type have exactly one? Is the type of the ...
Greg Nisbet's user avatar
  • 2,711
10 votes
2 answers
186 views

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

We can derive eliminators (as functions) for inductive types and translate (structurally) recursive functions into invocations of eliminators. However, eliminators seem to be essentially recursive ...
ice1000's user avatar
  • 5,877