Getting class instance with a placeholder

Stream: general

[Tomas Skrivan]

When class parameter is not marked as [inst : class_type] but as (inst : clas_type). Is there a way to use placeholder _ to fetch an instance of that class automatically.

An example, I want to define coinduced topology on a space X by a given function from reals. However, the topology on reals should be provided explicitly to the function coinduced curve "Topology on R". I was hoping that I can just write _, but this does not work:

import topology.instances.real

constants (X : Type)
def curve : ℝ → X := sorry

noncomputable def t1 : topological_space X := topological_space.coinduced curve _

Gives an error

/home/.../src/test.lean:6:80: error: don't know how to synthesize placeholder
context:
⊢ topological_space ℝ

It took me a long time to figure out how to get an instance manually

noncomputable def t2 : topological_space X := topological_space.coinduced curve real.metric_space.to_uniform_space.to_topological_space

I can write a simple helper function fetch_instance.

def fetch_instance {cls : Type} [t : cls] := t
noncomputable def t3 : topological_space X := topological_space.coinduced curve fetch_instance

What is the standard way to do this?

[Reid Barton]

(by apply_instance) should work in place of the _

[Eric Wieser]

Your fetch_instance is exactly docs#infer_instance

[Reid Barton]

src#infer_instance is also defined with the same definition as your fetch_instance, but I think it's disfavored for some reason.

[Tomas Skrivan]

Is there a fundamental problem with using _ instead of infer_instance? It would be quite intuitive.