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/