has_coe or id

Stream: Is there code for X?

[Yaël Dillies]

Is there any way to tell Lean that we have either α = β or has_coe_t β αand that we should either use no coercion (or the identity coercion?) or the coercion given by has_coe_t β α?

[Yaël Dillies]

Another way to see my problem is that we don't have has_coe_t α α. Maybe to avoid Lean trying to always coerce everything?

[Anne Baanen]

Can you give an example of how you would apply this? If you're defining a declaration for example, is there a reason that it wouldn't work to take a parameter of type α and letting the elaborator do the coercion at the point of use?