Skip to main content

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].

1 question with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
7 votes
0 answers

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 (...
Trebor's user avatar
  • 3,967