Frédéric Blanqui
Frédéric Blanqui
make sanity_check fails. Thanks to fix it.
This PR is probably too old now. It should be completely rewritten after #328.
The problem is that the rangemap is built from the AST where non-qualified identifiers have not been resolved yet as it depends on which modules are open and in which...
Yes, this is already done in https://github.com/ocaml-community/sedlex/issues/96. But sedlex developers did not answer yet.
Thank you very much @htzh for reporting these problems. This is very helpful to improve Lambdapi. Perhaps @firewall2142 could provide some workaround for problem 3. In Emacs, it is possible...
Could you please give your inductive type definition? The command "inductive" doesn't work?
I see. Thank you. I am going to see what can be done (extending inductive to strictly-positive types is also in our agenda). Just a few remarks on your code:...
@dwarfmaster Note that it is already possible to use `let`'s in a RHS so that you can write: ``` rule ind $case1 $case2 $case3 ... $case20 (constructorN $rec1 $rec2) -->...
Well, finally, I am soon going to add strictly-positive inductive types in master. I already have a local branch working. I just need to do a few more tests and...
Let's keep it open for the record.