Alessio Coltellacci

Is this issue still open? ``` symbol A: TYPE; symbol f : A → A → A; symbol {|i$|}:A; injective symbol + : A → TYPE; opaque symbol test: Π...

Oh sorry I forgot that I was in `Lambdapi version: dev-2.1.0-116-g93668def` because of #843, so I also got the error ``` "{|i@|}": Escaped identifiers or regular identifiers having an integer...

> the order of elements should not be relevant. But we then get problems with unification yes, I have a unification error, and I agree that the order should not...

> This can be fixed by recanonizing terms after each Bindlib substitution, which would be very inefficient. Yes, it sounds not a very desirable solution, especially in my case where...

The reconstruction of `resolution` seems to work https://gist.github.com/NotBad4U/47eeda2d489fd595a368a509d3bde7a5. I just lost the type inference but I guess it is because the PR is a WIP.

> The reconstruction of resolution seems to work Yes, I said it worked 😄 : _"The reconstruction of resolution seems to work..."_ > Please add an example where type inference...

> Please add an example where type inference does not work. In this case, the inference does not work, and the problem does not come from the modifier `associative commutative`...

But in this case, the symbol ⟇ will not have a definition and just exists at the syntactic level. An interesting solution will be to be able to define ⟇...

Okay thx for the answer, > If ⟇ is commutative then ⟇ cannot be constant nor injective: a ⟇ b = c ⟇ d has 2 solutions: (a,b)=(c,d) and (a,b)=(d,c)....

What do you consider the easiest to do in a short time? > Translate Lambdapi tactics to Coq tactics. The Lambdapi tactic is very similar to the Coq tactic so...