Richard Moot
Richard Moot
Currently, the proof output produces long normal form proofs (ie. beta-normal eta-long proofs). This makes sense from the point of view of proof search, but can be more user-friendly to...
Forall links have the property that no atom containing the eigenvariable of a link can every be identified with a node which dominates the forall link of this variable. Adding...
Allow specification of constraints of the form X=
Add additives together with a contraction condition as proposed by Maieli. This will be a major update/rewrite since it will complicate (at least) the axiom linking component: it will allow...