Stream: general

Topic: Coercion of pi types by coercing their return type

Eric Wieser (Nov 10 2020 at 17:00):

Currently, lean/mathlib won't automatically coerce f : Π 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_coe instance 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