Questions tagged [extensional-type-theory]
Use for proof assistants or type theories featuring an equality type that has a reflection rule creating judgemental equalities out of them. See also [reflection].
2
questions with no upvoted or accepted answers
7
votes
0
answers
146
views
Tutorial implementations of extensional type theories
There are cool projects out there that covers the basic principles of implementing dependent type theories as very spartan proof assistants. These projects helped a lot when I learned about (...
- 3,688
4
votes
0
answers
60
views
What is the state of Nuprl and Extensional Type Theory?
I want to use extensional type theory. I have installed Nuprl (on a virtual machine). It starts over an hour and I can't find examples or forums. Is there a better way?
