eliminators are proof relevant eliminations.
From comment by Andrej Bauer
Eliminators are proof relevant eliminations.
From comment by Kevin Buzzard
A constructor for X is a way of making things of type X, and an eliminator for X is a way of using things of type X to make other stuff (i.e. a way to make functions from X to other types).
|
created |
2 years, 10 months ago |
|
viewed |
3 times |
|
active |
2 years, 10 months ago |
|
editors |
1 |
