Add axioms of intuitionistic logic to Heyting algebras

[sacsar]

I'd appreciate feedback on what to call these functions (and anything else, obviously). I took the names from Wikipedia, but they feel decidedly clumsy.

[mikeizbicki]

Oops! I didn't see this until just now. Sorry about that :(

The axioms themselves look good. There's two changes to make.

1. Modify the names so that they start with theorem instead of axiom. These laws can all be proven from the Heyting laws that begin with law, so they are "theorems."
2. Add these theorems to the test suite at https://github.com/mikeizbicki/subhask/blob/master/src/SubHask/TemplateHaskell/Test.hs#L63, this will both double check that the theorems are written correctly and that all the current instances of Heyting are correct.

[sacsar]

Mentioning that I've seen this, but won't get to it for another week or so.

[mikeizbicki]

I can't merge the changes until the travis checks pass.

[sacsar]

First I have to figure out what the error means...

[sacsar]

Is there an idiot's guide to figuring out how the tests work (besides what's in the readme)?

I'm failing with
‘theorem_Heyting_then1’ is not in scope at a reify In the splice: $(mkSpecializedClassTests [t| Bool |] [''Enum, ''Boolean])
but I have no idea how to get it (and presumably the other theorem methods) into scope.

[sacsar]

@mikeizbicki It took me long enough, but the tests actually pass now.