Zulip Chat Archive
Stream: triage
Topic: issue !4#24099: chore: restore the binder overrides for s...
Random Issue Bot (Sep 09 2025 at 14:12):
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?
Random Issue Bot (Jan 12 2026 at 14:14):
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?
Last updated: Feb 28 2026 at 14:05 UTC