Dedukti Why Reduction.are_convertible_lst calls term

Why Reduction.are_convertible_lst calls term_eq ?

Open fblanqui opened this issue 2 years ago • 5 comments

This has been pointed to me by @01mf02. It looks useless and inefficient. The code of conversion_step looks strange too (calls to snf).

Jun 15 '22 16:06 fblanqui

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 is necessary but there is a TODO above.

Jun 16 '22 12:06 francoisthire

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

Jun 16 '22 12:06 francoisthire

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

Jun 16 '22 12:06 gabrielhdt

I see. It would be good to add a comment about this in the code.

Jun 16 '22 12:06 fblanqui

I have updated #280 with a comment.

Jun 16 '22 14:06 francoisthire