lambdapi
lambdapi copied to clipboard
Deducteam
Proof assistant based on the λΠ-calculus modulo rewriting
``` 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...
The translation of types to Why3 introduced in #769 is unsafe: we must ensure that the types translated as fresh constants in Why3 are inhabited. See https://github.com/Deducteam/lambdapi/pull/769#discussion_r772928743 for the original...
``` 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...
running `dune build @fmt` prints ``` ocamlformat: Error while parsing .ocamlformat: For option "version": expecting "0.19.0" but got "0.15.0" ```
``` 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 '_'. ```
# Symptoms Lambdapi raises `assert false` when the `package_path` of the related `lambdapi.pkg` changes and that another file from the same package is imported (from a `lpo`). # How to...
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...
We will need to handle dependencies separately to make things work for the editor mode (or rather, LSP server) developed by @ejgallego. In particular, we need to change the way...
@amelieled Hi ! Do you use emacs or vscode ? Have you been able to use emacs lsp mode on tests/OK/inductive_type.lp (it's freezing on my laptop) thanks can someone reproduce...
