coercion

Stream: lean4

[Kenny Lau]

How does coercion work in Lean 4, and how does it differ from the Lean 3 approach? I have noticed that Lean 4 has these extra classes for coercion: CoeT, CoeHead, CoeTail, CoeDep; while Lean 3 has the extra has_coe_t_aux.

The other classes should correspond as follows:

has_coe: Coe
has_coe_t: CoeTC
has_coe_to_fun: CoeFun
has_coe_to_sort: CoeSort