[Haskell-cafe] haskell-curry, classical logic, excluded middle
newsham at lava.net
Mon Oct 15 02:27:19 EDT 2007
> 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:
and example theorems:
Should this go up on the wiki somewhere?
More information about the Haskell-Cafe