Definition
Instance synthesis (Lean)
Instance synthesis is Lean’s search for a term of a requested class type. It considers available local and registered instances, matches their result types against the requested type, and recursively searches for any instance arguments they require.
Elaboration uses this search to fill omitted instance-implicit arguments. It does not search every term or prove arbitrary propositions: a suitable instance must be available and its requirements must be resolved.