search

mikeizbicki / subhask

Type safe interface for working in subcategories of Hask
BSD 3-Clause "New" or "Revised" License
418 stars 43 forks source link

Add axioms of intuitionistic logic to Heyting algebras #41

Open sacsar opened 8 years ago

sacsar commented 8 years ago

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 commented 8 years ago

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 commented 8 years ago

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

mikeizbicki commented 8 years ago

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

sacsar commented 8 years ago

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

sacsar commented 8 years ago

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 commented 7 years ago

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