[Haskell-cafe] haskell-curry, classical logic, excluded middle

[Tim Newsham]

> 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 haskell types
now, using an identical interface/notation (ie. they're swappable
for proofs that don't need excluded-middle).  The interfaces use
infix type names that "read" similarly to their meanings:

logic:
   http://www.thenewsh.com/%7Enewsham/formal/curryhoward/IntLogic.hs
   http://www.thenewsh.com/%7Enewsham/formal/curryhoward/ClassLogic.hs
and example theorems:
   http://www.thenewsh.com/%7Enewsham/formal/curryhoward/IntTheorems.hs
   http://www.thenewsh.com/%7Enewsham/formal/curryhoward/ClassTheorems.hs

Should this go up on the wiki somewhere?

Tim Newsham
http://www.thenewsh.com/~newsham/