Diffusion afp-devel 999b71d9f41d

fix(ML_Unification) replace binders before aeconv (avoids lowering)
999b71d9f41d
Actions

Tags

None

Subscribers

None

Description

fix(ML_Unification) replace binders before aeconv (avoids lowering)

Details

Provenance

Authored on

Parents

rAFPe1dd89a2f035: feat(ML_Unification) add simplification+unification unifier; fix context merge…

Branches

Unknown

Tags

Unknown

Event Timeline

kappelmann committed rAFP999b71d9f41d: fix(ML_Unification) replace binders before aeconv (avoids lowering).Mar 22 2024, 4:15 PM

Changes (1)

Path

Size

thys/

ML_Unification/

Unifiers/

simplifier_unification.ML

rAFP999b71d9f41d

thys/ML_Unification/Unifiers/simplifier_unification.ML

Loading...