On Fri, Apr 3, 2015 at 1:39 PM, Matt Oliveri <[email protected]> wrote: > On Fri, Apr 3, 2015 at 8:02 AM, Keean Schupke <[email protected]> wrote: >> On 3 April 2015 at 12:21, Matt Oliveri <[email protected]> wrote: >>> This is due to the HOAS semantics. Again, you cannot expect to go >>> about all of math in this manner. >> >> Please provide an example. I think you can derive the whole of maths :-) > > Well, I'm worried you'll just misunderstand the task, but that would > hopefully clarify the misunderstanding, at least. I'll put it in > another email.
Define two predicates on natural numbers, even and odd: even : nat->type even_z : even z even_ss : even N->even (s (s N)) odd : nat->type odd_sz : odd (s z) odd_ss : odd N->odd (s (s N)) (I'm not sure those are valid Twelf, but you know what I mean.) Prove that any natural number that isn't even is odd. For starters how would you _express_ that proposition, seeing that LF doesn't have negation or falsehood? No, proving that every number is either even or odd is not good enough. The point is you're missing negation. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
