# Zulip Chat Archive

## Stream: new members

### Topic: Abstracting types in constructors

#### Ruben Lapauw (Jan 13 2021 at 23:47):

I want to abstract a complex type by introducing a "newtype". How can I pass the implicit variables implicitly?

```
variables {x:nat}
structure nt: Type := (data: fin x)
--Works
structure foo := (v : list (@nt x))
--Error:
-- don't know how to synthesize placeholder
-- context:
-- x x : ℕ
-- ⊢ ℕ
structure foo := (v : list nt)
```

Edit: smaller MWE

#### Eric Wieser (Jan 13 2021 at 23:51):

What are you expecting the last line to do? How would lean know to pass `x`

to `@nt`

and not `37`

?

#### Ruben Lapauw (Jan 13 2021 at 23:53):

The same way lean knows x is available when proving theorems? I don't need to specify most type-variables in those proofs.

#### Eric Wieser (Jan 14 2021 at 00:07):

Can you give an example of the case you're thinking of that does work, so that I can explain the difference?

#### Ruben Lapauw (Jan 14 2021 at 00:12):

```
lemma inf_lt {A : set ℝ} {x : ℝ} (hx : x is_an_inf_of A) :
∀ y, x < y → ∃ a ∈ A, a < y :=
```

is used like this:

(https://github.com/leanprover-community/tutorials/blob/0a0de42dd339de62b1e781745fd128afba4d1df8/src/solutions/00_first_proofs.lean#L398)

```
apply inf_lt h,
```

in which A and x are implicit.

#### Eric Wieser (Jan 14 2021 at 00:13):

Right, that's because `h`

contains `x`

and `A`

as part of its type

#### Eric Wieser (Jan 14 2021 at 00:14):

If you know the type of `h`

, then lean has only one possibly choice for those implicit variables - so it makes that choice

#### Eric Wieser (Jan 14 2021 at 00:17):

Having said that, you can probably get what you want with `parameters {x : nat}`

which I think tells lean "treat x as a constant in the current section".

#### Ruben Lapauw (Jan 14 2021 at 00:20):

yeah, thats exactly what I want!

But continuing with the problem:

Thus if I had:

```
variable {x :nat}
structure nt {y: nat} (x=y) : Type := (data: fin x)
```

then

```
structur foo := (v: list (nt ($$$))) -- With $$$ a proof that x=x
```

would work? Since in this proof there is a variable which is then unified with the unknown 'x'?

#### Ruben Lapauw (Jan 14 2021 at 00:32):

Curiouser and curiouser: with parameters the second example works, but not the first. This I can somewhat understand. However their type makes me very confused. How can I see their full type?

```
section s
parameters {x:nat}
variable {y: nat}
structure ntx: Type := (data: fin x)
structure nty: Type := (data: fin y)
#check ntx -- ntx : Type
#check nty -- nty : Type
end s
```

#### Kevin Buzzard (Jan 14 2021 at 00:42):

Outside the section try `#check @ntx`

#### Ruben Lapauw (Jan 14 2021 at 00:45):

And inside or outside for @nty.

Thank you both!

Last updated: May 06 2021 at 22:13 UTC