Frédéric Blanqui
Frédéric Blanqui
@amelieled what happens if you use https://github.com/Deducteam/lambdapi/pull/308 ?
I believe that, in Gabriel's mode, you must not add (load "lambdapi"). @gabrielhdt do you confirm? This is perhaps the reason why it is looping.
Well, I am not sure anymore because, if I do not add (load "lambdapi"), then it doesn't work.
Why should we use package-delete?
How is it possible to add a rule to a definition? This should generate an error! This is a bug.
No, this is not a bug. It's perfectly fine to write this, syntactically, except that it does not terminate. @amelieled , simply write `definition N := \tau nat` or `symbol...
Hi @Rehan-MALAK . Woah! How did you get this graph? It's nice. Do you have a solution for #154?
@Rehan-MALAK even if this requires quite some manual tuning, I think that it would be better to put this in tools/depgraph/ for instance with some README.md. Could you please make...
See remark by @amelieled (https://github.com/Deducteam/lambdapi/issues/705#issuecomment-857503964): It's a bit strange, because if I understand correctly, you can write: C.lp: ``` symbol c : TYPE; ``` B.lp: ``` require open tests.C; symbol...
https://github.com/Deducteam/lambdapi/blob/1fb1d9aa8d162279e0496d976b286fffc721f332/src/core/unif.ml#L408-L410 Unification in LP is only intended to be correct and predictable. As unification modulo rewriting is undecidable and may have many solutions, we only ask to try to return...