lean implicits

Stream: lean4

[Oleg M]

Where can I read about Lean's implementation of implicits? I saw a paper on typeclasses, but, sadly, couldn't find anything very descriptive for implicits.

Thank you very much for answering.

[Mario Carneiro]

Modulo a lot of technical details, the basic algorithm by which implicit arguments and metavariables generally are solved is called (first-order) unification. See https://en.wikipedia.org/wiki/Unification_(computer_science)

[Oleg M]

Thank you!