lambdapi
lambdapi copied to clipboard
Deducteam
Proof assistant based on the λΠ-calculus modulo rewriting
Rewriting generates holes that must be transformed into existential variables by the type checker. Unification hints have been adapted to use that mechanism. Fixes issue #600 There is also a...
Simple coercions TODO - [x] use a better strategy than SNF to reduce coercions - [x] ensure holes generated by coercion are properly transformed into existential variables This pull request...
``` symbol A:TYPE; symbol B:TYPE; symbol C:TYPE; symbol a:A; unif_rule A ≡ B ↪ [ A ≡ Π x:C, $m[x] ]; symbol b : B ≔ begin print; refine a;...
This pull request allows the rewriting engine to match on constant `TYPE`. This will allow to create coercions of the form ``` coercion coerce Set $x TYPE --> El $x;...
``` 16:47 ~/src/lambdapi (db) lambdapi check --no-col 16:51 ~/src/lambdapi (db) lambdapi check --blabla lambdapi: unknown option `--blabla'. Usage: lambdapi check [OPTION]... [FILE]... Try `lambdapi check --help' or `lambdapi --help' for...
This pull request adds a coercion mechanism on top of the new typechecker. Adding such a mechanism involves: - creating a new symbol in its own signature that stands for...
In some cases, it is possible to use implicit arguments to build a term which can be elaborated into different terms having different types (modulo =_R). It seems that, when...
``` constant symbol A : TYPE; constant symbol a : A; symbol f : A → A; rule f $x ↪ $x; rule f _ ↪ a; [/home/blanqui/src/lambdapi/tmp/dup_cp.lp:6:0-13] Unjoinable critical...
``` symbol T:TYPE; constant symbol arrow : T → T → T; constant symbol L : T → TYPE; symbol app a b : L (arrow a b) → L...
I tried to follow the tutorial after ```opam install``` on a Mac. I have observed the following problems: 1. In `vscode` LSP server would not start until I created the...
