Frédéric Blanqui
Frédéric Blanqui
Hi. Yet, opam info indicates: "ocaml" {>= "4.08.0"} "dream-httpaf" {>= "1.0.0~alpha2"} I have many CI currently failing because of this issue: https://github.com/Deducteam/lambdapi/actions/runs/14725968105/job/41328568312?pr=1241 https://github.com/Deducteam/lambdapi/actions/runs/14623864154/job/41030513500?pr=1237 https://github.com/Deducteam/lambdapi/actions/runs/14622423369/job/41025610782?pr=1129 Do you have any idea on...
Hi. FYI, I tested all possibilities: https://github.com/Deducteam/lambdapi/actions/runs/14729052162/job/41338640569
Versions of ocaml, dream-pure, dream-httpaf, dream that work: ``` 4.09.1, 1.0.0~alpha1, 1.0.0~alpha1, 1.0.0~alpha3 4.09.1, 1.0.0~alpha2, 1.0.0~alpha1, 1.0.0~alpha4 4.09.1, 1.0.0~alpha2, 1.0.0~alpha2, 1.0.0~alpha5 4.09.1, 1.0.0~alpha2, 1.0.0~alpha2, 1.0.0~alpha6 4.09.1, 1.0.0~alpha2, 1.0.0~alpha3, 1.0.0~alpha5 4.09.1,...
Hi Jean-Paul. Thanks for your issue, and your suggestion. Note also that in case you have problems with apply, you can always use refine instead. But your tactic call is...
I still don't understand why you would like to do some apply that does not change the goal. And this doesn't correspond to the semantics of (apply t), which is...
You'll see it if you do make tests: this is in the stdlib.
> the purpose of the apply was to change the goal into an equivalent one modulo rewriting rules by giving a type to the parameter h. Do you mean a...
@NotBad4U Could you please try this PR on some other examples for linear arithmetic ?
Be careful that I changed the ordering: arguments are now compared from left to right. So, you need to permute the arguments of var.