Frédéric Blanqui
Frédéric Blanqui
Does that mean that meta rules must preserve typing?
Hi @gabrielhdt . Michael's suggestion looks nice and easy to implement. Do you want to try it? I will then wait for the version 5.1 of pratter and an update...
Hi @gabrielhdt . I see that pratter 5.0.1 is now available on opam. Could you please update your PR so that I can merge it?
The 1st item has been done in https://github.com/Deducteam/lambdapi/pull/1215. The items 3 and 4 are not related to the eval tactic itself. Item 3 is related to #217. Item 4 is...
Hi Alessio. This is currently not possible as it is formulated since `#refine` takes a term as argument and curly brackets are not part of the syntax of terms. You...
Hi Alessio. Do you mind if I close this issue, which is not actually one? I prefer to reserve issues for actual and precise issues. You can use the Discussions...
I suggest that you generate a file with lpo dependencies that you include in your Makefile (see #1108): it will be more optimal and may solve your problem (this is...
Example: in your Makefile, add: ``` include lpo.mk LP_FILES := $(wildcard *.lp) lpo.mk: $(LP_FILES:%.lp=%.lpo.mk) find . -maxdepth 1 -name '*.lpo.mk' | xargs cat > $@ %.lpo.mk: %.lp dep-lpo $*.lp ```
PS. As you generate the lp files, it doesn't cost much to generate the .lpo.mk files as well at the same time, so that you don't need dep-lpo. This is...
Is it fixing #295 too?