Gabriel Hondet

Perhaps implicits: the first argument of `eq` is marked as implicits, so it should be ``` ∀n, π (eq {nat} n n) ``` shouldn't it?

If you want to remove the lambdapi emacs mode.

I can reproduce: `lambdapi check ` loops with the implicit argument added.

Ah! I found the culprit, ``` definition N ≔ τ nat rule τ nat → N ``` The `definition` is like a rewrite rule, so you have a non terminating...

I think you can't add `rule N -> ...` but I am not sure we want to forbid rewriting terms that are themselves definitions.

> That is not normal, you should be able to stop the LSP server somehow. Or at least to tell the LSP mode to stop sending updates for a while....

For this issue (as for coercions), a possible solution is to have the rewrite engine generate holes, and then infer the type of the generated term in order to replace...

It's not the first time it happens, perhaps we should check the awk version with a `awk --version | grep GNU` or something of the kind...

It seems to me that as of https://github.com/Deducteam/lambdapi/pull/809/commits/d405f4d3aa8c11e604ce0df765390449bb2c6a17, the algorithm is ready. What lacks is to be able to parametrise reduction to not reduce protected symbols. But this can be...

There seem to be no impact performance-wise.