Eric Wieser (Nov 10 2020 at 17:00):
Currently, lean/mathlib won't automatically coerce
Π i j, i ≤ j → G i →+* G j to
Π i j, i ≤ j → G i → G j, which requires me to write the clumsy
(λ i j h, f i j h) whenever I want the coercion.
- Is this something we should fix by defining a
has_coeinstance for pi types in mathlib?
- Is this something that lean 4 could improve?
- Or is having this happen automatically just a bad idea?
Last updated: May 10 2021 at 19:16 UTC