Checking Expr equality

Stream: Is there code for X?

[Adam Topaz]

Do we have a variant of docs#Lean.Expr.equal that checks for equality of binder kinds (i.e. default vs implicit etc), but ignores equality of binder names?

[Kyle Miller]

Not that I know of, but you could at least normalize all binder names to, say, a, and then use Lean.Expr.equal.

[Adam Topaz]

Do we have any convenient way to normalize all names, or do I have to dig into the Expr manually?

[Kyle Miller]

I expect you'd have to dig (and also might want to use caching to make sure subexpressions are shared, in case that sort of performance consideration matters!)

[Adam Topaz]

Do you know of any code that does such caching for me to look at as an example?

[Kyle Miller]

If you use docs#Lean.Core.transform to do this renaming, it'll use caching automatically.

[Adam Topaz]

Awesome. Thanks Kyle!

[Kyle Miller]

You can use a post method for that, and you can return .continue with the updated expression (or .done, it doesn't matter for post)