Slightly offtopic - I am curious about the use of forall in some type signatures:
If you specify the "forall p q" at the top level then the types used internally will use the same "p" and "q". Otherwise the internal types will be new "p"s and "q"s and wont line up with the outer type declaration.
subsume :: forall p q r. Prop (p :=> q) -> Prop ((p :/\ q) :== p) subsume pIMPq = equivInj (impInj pq2p) (impInj p2pq) where pq2p :: Prop (p :/\ q) -> Prop p pq2p assumePQ = andElimL assumePQ p2pq :: Prop p -> Prop (p :/\ q) p2pq assumeP = andInj assumeP q where q = impElim assumeP pIMPq
There "r" type variable is mentioned, but it does not occur anywhere else in the signature - what's the purpose of this construct?
Ahh! "r" is a remnant of earlier iterations where I had carried around the "r" in every CProp from the classical propositions. Then I realized I could just pick any "r" (I picked "()") and avoid having to type "r" everywhere. So its no longer used, and I'll remove it from the code and the paper. Thank you!
Krzysztof Kościuszkiewicz Skype: dr.vee, Gadu: 111851, Jabber: kokr@jabberpl.org Mobile IRL: +353851383329, Mobile PL: +48783303040 "Simplicity is the ultimate sophistication" -- Leonardo da Vinci
Tim Newsham http://www.thenewsh.com/~newsham/