Zulip Chat Archive

Stream: lean4

Topic: coercion


view this post on Zulip Kenny Lau (Jan 07 2021 at 08:39):

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

Last updated: May 18 2021 at 22:15 UTC