# Zulip Chat Archive

## Stream: general

### Topic: Getting class instance with a placeholder

#### 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?

#### Reid Barton (Oct 20 2020 at 16:17):

`(by apply_instance)`

should work in place of the `_`

#### Eric Wieser (Oct 20 2020 at 16:19):

Your `fetch_instance`

is exactly docs#infer_instance

#### 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.

#### 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