jonsterling / tt-singletons

experiments with singleton types & identity types in type theory
MIT License
3 stars 0 forks source link

Add booleans #5

Closed jonsterling closed 9 years ago

jonsterling commented 9 years ago

Heh. It's becoming quickly apparent why Conor put that "aspects on the cheap" stuff into SHE. Must be nice to be able to define all the stuff for a new type all at once. In fact, the Epigram 2 source is very informative in that way, since you can see at a glance everything you need to know about something like quotients, etc.