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

      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:

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