jgonggrijp / net-prove

Academic theorem prover based on proof nets, focused on LG, written in Haskell.
Other
3 stars 2 forks source link

Use `Either Bool Link` instead of `Maybe Link` in `NodeInfo` #6

Open digitalheir opened 9 years ago

digitalheir commented 9 years ago

Either Bool Link instead of Maybe Link in NodeInfo's link field, so we can denote whether a leaf node is 'accepting' of node identifications. Original hypothesis and conclusion node are 'closed' (False), while all other leaf nodes are 'open' (True).

I volunteer to make this edit.

jgonggrijp commented 9 years ago

You mean Either Bool Link, right? ;-)

digitalheir commented 9 years ago

Uhhh, yeah. I'm working on feature branch for it right now; need to adapt a bunch of code that still depends on Maybe Link.

digitalheir commented 9 years ago

Please see branch feature-bool-link-type. We need a Unifiable instance for the new type NodeLink.

I don't really understand the Unifiable code, so I'm afraid to touch it.