Zulip Chat Archive

Stream: lean4

Topic: function coercions in the stdlib


view this post on Zulip Jason Gross (Mar 12 2021 at 19:41):

Is there a reason the standard library doesn't have coercion instances such as

instance CoeArr {α β α' β'} [Coe α' α] [Coe β β'] : Coe (α  β) (α'  β') := { coe := λ f a => coe (f (coe a)) }

?

view this post on Zulip Mario Carneiro (Mar 12 2021 at 20:27):

I personally think it's better to be explicit about such things; it's also more work to unravel the coercions in simp or what have you

view this post on Zulip Mario Carneiro (Mar 12 2021 at 20:28):

Plus instances like this are an easy way to accidentally sneak transitivity into a typeclass that isn't supposed to be transitive

view this post on Zulip Mario Carneiro (Mar 12 2021 at 20:28):

(this is an issue that has bit us before in mathlib)

view this post on Zulip Jason Gross (Mar 12 2021 at 20:29):

I'd be fine with replacing Coe with CoeTC in all the places, and then the transitivity issue isn't a problem...


Last updated: May 18 2021 at 22:15 UTC