Frédéric Blanqui
Frédéric Blanqui
``` 11:41 ~/src/lambdapi (master) \rm tests/OK/*.lpo 11:41 ~/src/lambdapi (master) dune exec -- lambdapi check -w -c tests/OK/why3_quantifiers.lp tests/OK/logic.lp tests/OK/bool.lp tests/OK/nat.lp Loading "/home/blanqui/src/lambdapi/tests/OK/why3_quantifiers.lp" ... Loading "/home/blanqui/src/lambdapi/tests/OK/logic.lp" ... Loading "/home/blanqui/src/lambdapi/tests/OK/bool.lp" ... Loading...
``` verbose 3; symbol A:TYPE;// the log panel should display: "(symb) A : TYPE" instead of nothing currently symbol a:A;// the log panel should display: "(symb) a : A" instead...
``` symbol A:TYPE; symbol app:(A → A) → A → A; rule app (λ x, $a.[x]) $b ↪ $a.[$b]; // Pattern variable b can be replaced by a '_'. ```
When, in Emacs, I want to look at a file f.lp located in /d1/d2/../dn/, I get no feedback if one of the directory di contains non-ascii characters.
Dedukti seems to allow to have a file f.dk containing: ``` symbol const N : TYPE symbol const z : f.N ``` Is it a desirable feature, or should we...
``` constant symbol Set : TYPE; injective symbol τ : Set → TYPE; constant symbol prop : Set; symbol Prop ≔ τ prop; injective symbol π : Prop → TYPE;...
Currently, the file tests/OK/gaspard.dk is accepted. Its LP version is: ``` constant symbol U : TYPE; constant symbol foo : U; constant symbol e : U → TYPE; constant symbol...
Currently, the generation of lambdapi.opam from dune-project has been deactivated, and the targets @runtest and @doc removed, because of problems with why3 config detect (see https://gitlab.inria.fr/why3/why3/-/issues/603).
By @QGarchery: ``` symbol test_rew_lambda f : π (`∀ a, `∀ b, f (a + b) ⇒ f b) ≔ begin // Does not rewrite under binders rewrite add_com; end;...