Instance search order?

Stream: general

[Yury G. Kudryashov]

In which order does Lean 4 generate instances? Is it possible to turn, e.g., docs#SmoothMul by adding an unused assumption [BaseField 𝕜] with no global instances of [BaseField] (with scoped instances for Real and Complex)? My idea is that someone can write haveI : BaseField K := .mk at the beginning of a proof and get instances like docs#SmoothMul docs#continuousMul_of_smooth, docs#FiniteDimensional.complete etc

[Eric Wieser]

I don't understand your last two doc links; the first is a class but the second is an instance

[Eric Wieser]

Did you have a particular SmoothMul instance in mind?

[Yury G. Kudryashov]

Fixed

[Yury G. Kudryashov]

BTW, should links to library notes work or doc-gen4 doesn't support library notes?

[Kyle Miller]

Separating the implementation idea from the problem: we have scoped instances, but it would be nice to have parameterized scoped instances, where you can specify values for arguments that can't be inferred during typeclass inference. The point would be that you can introduce multiple instances simultaneously, rather than one at a time by name.

Yury's idea: have a dummy class with the additional parameters, and make some classes require this class as an extra argument. The assumption is that all instances of such classes would need these parameters anyway (if I understood correctly).

[Kyle Miller]

(By the way @Yury G. Kudryashov, in Lean 4 haveI now means "have and inline the value", and have by itself can now introduce instances. No more unfreezingI and friends)

[Yury G. Kudryashov]

If k is Real or Complex, then it's easy to have scoped instances specializing a general instance to this field. It's more complicated if k is a local variable.