fthire

> LP is intended to be a proof assistant, not a rewrite engine. So, in this context, these rewrite rules are not acceptable. Hence, we have to consider that the...

> François, Dedukti itself has never been thought as a rewriting engine alone. What you are talking about is not Dedukti, but dkmeta, the rewriting part of Dedukti. So, yes,...

Indeed, contribution are welcome but in short: - `#REQUIRE` is not mandatory but in some cases it is necessary (a rule in a file which depends on another rule, declared...

I suspect that if the top symbol of a rule (the symbol rewritten) is declared as `ac` or `acu` then we have matching (or filtering?) which is done `ac` or...

See #280 for a partial answer. It does not seem useless nor inefficient. The call to `snf` was introduced by @Gaspi for the AC feature. I cannot explain why this...

I would be curious to know how `lambdapi` behaves on the test `tests/OK/sharing.dk`.

I have updated #280 with a comment.

`#NAME` was deprecated, the time the libraries could be adapted. `#REQUIRE` is not necessary but I know some situations where it is necessary. Assume I have three modules (dk files):...

@fblanqui can this issue be closed? What do you expect to solve it otherwise?

@Gaspi , any plan to solve this?