Now that that works, one more question. Is it possible to hide the r that
is attached to every single type? For example to do something like this
(which doesn't compile):
No answer needed. Duh.. I can just pick r to be any type (like ()).
I've got intuitionistic logic and classic logic in
I've been struggling with this for the last day and a half. I'm
trying to get some exercise with the type system and with logic by
playing with the curry-howard correspondence. I got stuck on
the excluded-middle, and I think now I got it almost all the way
there, but its still not quite right.
On 10/14/07, Tim Newsham [EMAIL PROTECTED] wrote:
I've been struggling with this for the last day and a half. I'm
trying to get some exercise with the type system and with logic by
playing with the curry-howard correspondence. I got stuck on
the excluded-middle, and I think now I got it
On Sun, 2007-10-14 at 15:20 -0600, Luke Palmer wrote:
On 10/14/07, Tim Newsham [EMAIL PROTECTED] wrote:
I've been struggling with this for the last day and a half. I'm
trying to get some exercise with the type system and with logic by
playing with the curry-howard correspondence. I got
You realize that Djinn can write all that code for you? :)
Well, not with your encoding of Not, but with a similar one.
-- Lennart
On 10/14/07, Tim Newsham [EMAIL PROTECTED] wrote:
I've been struggling with this for the last day and a half. I'm
trying to get some exercise with the type
On Sun, 14 Oct 2007, Roberto Zunino wrote:
(Warning: wild guess follows, I can not completely follow CPS ;-))
Adding a couple of forall's makes it compile:
propCC :: ((forall q . p - Prop r q) - Prop r p) - Prop r p
func1 :: (forall q . Or r p (Not r p) - Prop r q)
- Prop r (Or r p (Not r
On Sun, 2007-10-14 at 17:19 -1000, Tim Newsham wrote:
On Sun, 14 Oct 2007, Roberto Zunino wrote:
(Warning: wild guess follows, I can not completely follow CPS ;-))
Adding a couple of forall's makes it compile:
propCC :: ((forall q . p - Prop r q) - Prop r p) - Prop r p
func1 :: (forall q
