Frédéric Blanqui

Adding integers does not allow tracing back symbols and rewrite rules. It should be easy to identify in the output what comes from the input. Concerning linearity, please fix your...

I cannot reproduce your error. I works for me with lambdapi 2.4.0 and master. Which version of lambdapi do you use? Perhaps you have some hidden invalid character in your...

I see now. The problem is caused by the colon at the end. This is strange indeed.

Strange. You do not get an error? ``` 13:28 ~/lambdapi (master) lambdapi check tmp/946.lp Checking "/home/blanqui/src/lambdapi/tmp/946.lp" ... [/home/blanqui/src/lambdapi/tmp/946.lp:6:22-28] "{|i@|}": Escaped identifiers or regular identifiers having an integer suffix with leading...

I can reproduce Thomas problem with: ``` constant symbol Prop:TYPE; injective symbol Prf:Prop → TYPE; constant symbol ∧ : Prop → Prop → Prop; notation ∧ infix right 30; symbol...

Thank you for your issue Fernando. This is definitely something to do indeed. I will try to do this in the coming weeks or in June or July.

-o lp calls Pretty, which works on p_terms. We should rename this mode raw_lp, and a add a new mode lp working on terms.

Hi Alessio. I am afraid this won't be possible since the way AC symbols are handled in Lambdapi is crucially based on the fact that terms are always in AC-canonical...

There is an unexpected bug in Lambdapi in the handling of AC symbols, perhaps related to Bindlib. It will probably take me more time than expected to fix this.

No, we shouldn't in unification allow decomposition of AC symbol applications; this is wrong. The problem is that some terms are not put in AC canonical form as expected. Actually,...