Gabriel Hondet

I'd say that we can also not mention command line options in the readme, and refer to the manpage generated by cmdliner (which could be published).

It is already at the root of the repository https://github.com/Deducteam/Dedukti/blob/master/syntax.bnf

It looks out of date, there is no mention of `injective`.

Yes it is https://github.com/Deducteam/Dedukti/blob/c65e7e66fe4bb8285db1856b8fe2a2532da2bd50/Makefile#L165

I'm currently working on the manipulation of the nonlinear constraints within the heuristic. A first implementation triggered the check each time a nonlinearity were encountered, I'm trying to be able...

On the other hand, convertibility checks are expensive, aren't they? So we might want to avoid triggering them, if we can.

I recently tried the sudoku, which contains a eq rule: ``` eq x x --> T eq x y --> F ``` which is a big problem if I don't...

I think your answer is there: https://github.com/Deducteam/lambdapi/issues/313

All right, I'll just inline some example file here to have a taste of it ``` (; OK ;) A : Type. def B := A. def C := A....

It seems to be the case, even in plain OCaml, `int_of_string "9223372036854775808"` fails.