Zulip Chat Archive

Stream: general

Topic: Getting class instance with a placeholder


view this post on Zulip Tomas Skrivan (Oct 20 2020 at 16:15):

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?

view this post on Zulip Reid Barton (Oct 20 2020 at 16:17):

(by apply_instance) should work in place of the _

view this post on Zulip Eric Wieser (Oct 20 2020 at 16:19):

Your fetch_instance is exactly docs#infer_instance

view this post on Zulip Reid Barton (Oct 20 2020 at 16:19):

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

view this post on Zulip Tomas Skrivan (Oct 20 2020 at 16:21):

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


Last updated: May 08 2021 at 19:11 UTC