GuillaumeGen

For me `unsatisfiable constraints` means that the equations will never be satisfiable, ie.: - `C t_1 ... t_n = D u_1 ... u_m` with `C` and `D` different constant symbols,...

It seems strongly related to #183 .

> But what ACU implies? Does that mean that matching is modulo ACU? More or less. I don't know what the exact definition of matching modulo ACU is, but the...

This syntax change requires an update of the `syntax.bnf` file (generated by a command like `make bnf`) and of the `README` (at least the "Commands" section, probably some other occurrences...

I strongly support the claim of @rainbyte that when a programmer lets blank lines or comments in the middle of their import list, they do it voluntarily and it carries...

In #1817 I made an example of using Asterius to build an "Hello world!" (not the simplest one) and generate a `.wasm` file.

The issue is that when trying to to type check your last rule, Dedukti infers the substitution ``` [Rule] Inferred typing substitution: v1[5](0 args) -> Issue.cons! v2[4] v3[3] v4[2] v0[6](0...

~~Well, things are more subtle than that, because this file is accepted, whereas it happens exactly what I described in the previous comment.~~ ``` Nat : Type. 0 : Nat....

`m[3](0 args)` means that it is the variable with identifier "m", with de Bruijn index 3 (last to be declared variable has index 0, and then it increases) and is...

I realize that my week-end messages only expressed a diagnosis without any action plan. First, my opinionated version of the diagnosis is that refusing this file is quite legitimate, but...