Frédéric Blanqui
Frédéric Blanqui
@rlepigre In term.ml, you mentioned in a comment that _Meta_full is harmful for efficiency and the last rule of ram_out.lp contains many metavariables. Could this be an explanation? Or there...
@dwarfmaster If you want, you can try my branch "let" in https://github.com/fblanqui/lambdapi. It improves the handling of let's so that failing.lp does not fail anymore. But there is still a...
Thank you @rlepigre and @dwarfmaster for your help.
Hello @dwarfmaster . Did you succeed in putting every thing in a single file and minimize it?
Effect on efficiency: | library | master | PR | % | | ------- | ------ | -- | --- | | focalide | 18s | 29s | +61% |...
Hi Quentin. He doesn't surprise me. The introduction of term refinement (in order to add coercions) was known to introduce an important slow down. See https://github.com/Deducteam/lambdapi/blob/master/CHANGES.md. How important is it...
This is problematic indeed. Unfortunately, we do not have the time to look after this at the moment. Gabriel is ending the writing of his PhD, and I am myself...
Sure, we can add them in tests. But please consider adding your LP developments on https://github.com/Deducteam/opam-lambdapi-repository.
Hello François. Note that, if you add the rule with double, and double is defined, then you have a (local) confluence problem: for your system to be confluent, you should...
Ok, I see. François, what are your examples with big normal forms?