Implicit conversion

Stream: lean4

[Leni Aniva]

How does the implicit conversion of some x: X into .some x: Option X work? If I have my own option-like type, how can I implement this implicit conversion?

[Henrik Böving]

Through docs#Coe and related type classes

[Tom]

This is a very good introduction covering the basics: https://leanprover.github.io/functional_programming_in_lean/type-classes/coercion.html