issue !4#24099: chore: restore the binder overrides for s...

Stream: triage

[Random Issue Bot]

Today I chose issue #24099 for discussion!

chore: restore the binder overrides for structures from Lean 3
Created by @Eric Wieser (@eric-wieser) on 2025-04-15
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?