Frédéric Blanqui
Frédéric Blanqui
https://github.com/fblanqui/lambdapi/blob/db/tests/OK/991.lp works with #843. So I invite you to use #843 instead for the moment.
No, that PR should work. It is less efficient but should work. Please add an example where type inference does not work.
``` symbol Prop:TYPE; associative commutative symbol +: Prop → Prop → Prop; constant symbol p:Prop; constant symbol q:Prop; symbol T: Prop → TYPE; symbol a x y: T(+ x y);...
In the case where ⟇ is not declared associative commutative, the problem is that ⟇ is declared as definable (there is no modifier) and not constant or injective and thus...
If ⟇ is commutative then ⟇ cannot be constant nor injective: a ⟇ b = c ⟇ d has 2 solutions: (a,b)=(c,d) and (a,b)=(d,c).
To understand what unification tries to do, add `debug +u;` just before. An equation of the form f t1 .. tn = f u1 .. un can be simplified to...
I see. Currently, the export to dk is done after compilation but compilation does not record the definition of opaque symbols to save memory. To avoid this problem, we should...
Hi Thomas. One solution is make a copy of your files, remove the opaque modifiers with sed, and export files. I'm working on having a dk output which does not...
This is a counter-example to what exactly? Lambdapi just tries to check that, when adding new rules, the typable critical pairs are joinable (which is not decidable). If it finds...