Docs on coercions in Lean 4

Stream: new members

[Kevin Sullivan]

I've read the Lean 4 manual here (https://leanprover.github.io/lean4/doc/). I've read the part on typeclasses. Where's the best place to find documentation on Lean 4 coercions, in particular (analogous to has_coe in Lean 3)?

[Calvin Lee]

There is the Coe typeclass, see https://github.com/leanprover/lean4/blob/master/src/Init/Coe.lean
I'm not entirely sure what has_coe is in lean3 since I've only done lean4, but I hope this points you in the right direction