Talk:Natural numbers with inequality

From The Twelf Project
Jump to: navigation, search

It would probably be a good idea to standardize on one name for the uninhabited type in our tutorials. My vote goes to "void" since that is its common name in type theory. I think "false" is not a good choice since we often have terms inhabiting a type called false (in an encoding of classical logic, for instance). "Absurd" seems a little hokey to me, but I don't have a good argument against it...  — Tom 7 13:28, 6 September 2006 (MST)

I'm all for void, I'll make a note of it in Twelf style guide, since that's exactly the sort of thing that goes in a twelf style guide. - TheTwelfElf 13:37, 6 September 2006 (MST)