Gabriel

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...

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;...

Adding coercions mechanism

3

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...

Extended identifiers

2

Identifiers may contain $, ? or |, but not /. They may not begin with $ or ?. The identifier | is not valid (since it's the VBAR).

Allowed characters in identifiers

6

The following line does not typecheck: ``` symbol foo/bar: TYPE; ``` and yield the following error message ``` [...] The proof is not finished. ```

Improve scoping of pattern variables not used in the RHS

1

The first argument of the `Patt` data type is an integer option which was once set to `None` at scoping if the variable was linear and not used in the...

Term transformation helper function

7

Introduce a function that allows to rewrite a term with a specific set of rewrite rules. In particular, it may be used to implement tactics that transform terms.

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...

ocamlformat is out of date

3

running `dune build @fmt` prints ``` ocamlformat: Error while parsing .ocamlformat: For option "version": expecting "0.19.0" but got "0.15.0" ```