Zulip Chat Archive

Stream: new members

Topic: Docs on coercions in Lean 4

Kevin Sullivan (Feb 12 2021 at 04:22):

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 (Feb 12 2021 at 18:39):

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

Last updated: Dec 20 2023 at 11:08 UTC