Zulip Chat Archive

Stream: new members

Topic: Does lean have syntactic unification of first-order terms


Eric Taucher (Dec 17 2021 at 13:34):

Does Lean (3) or Lean4 have/implement the unification algorithm for first-order terms? (ref)

I know there is unification modulo definitional equality (ref), which is not what I seek.

Marcus Rossel (Dec 17 2021 at 15:42):

Maybe Section 2.2 of https://arxiv.org/pdf/1505.04324.pdf could help you (I'm not well versed in this topic).


Last updated: Dec 20 2023 at 11:08 UTC