Frédéric Blanqui
Frédéric Blanqui
Hi. In realax.ml, line 248, are introduced "nearly additive" functions but, on line 928, they are called "nearly-multiplicative".
cannot install `dream.1.0.0~alpha6` with `dream-httpaf.1.0.0~alpha4` with opam when using ocaml 4.12.1, 4.11.2, 4.10.2 or 4.09.1 ``` ∗ installed dream-httpaf.1.0.0~alpha4 [ERROR] The compilation of dream.1.0.0~alpha6 failed at "dune build -p dream...
Following https://github.com/aantron/dream/issues/390, here are the versions of ocaml, dream-pure, dream-httpaf and dream that work on 06/06/25 (https://github.com/Deducteam/lambdapi/actions/runs/15489333006): ``` 5.03.0, 1.0.0~alpha2, 1.0.0~alpha4, 1.0.0~alpha8 ``` and on 29/04/25 (https://github.com/Deducteam/lambdapi/actions/runs/14729052162): ``` 4.09.1, 1.0.0~alpha1,...
- ctxt: remove unused functions
This PR reimplements conversion modulo AC without enforcing terms to be in AC-canonical form. This is much more efficient but may not work with any rewrite system. It seems to...
test the various versions of all the dependencies: emacs, eglot, math-symbol-list, highlight using editors/emacs/test.sh
TODO: - [ ] update CHANGES - [ ] update doc (including limitations) - [ ] extend to dk files - [ ] test - [ ] try to handle...
TODO: - [x] factorize the beginning of coq.ml and lean.ml into stt.ml - [x] update doc - [ ] in Lean.print: prefix namespace by root_path