## Stream: general

### Topic: Providing implicit arguments to a function field

#### Lime Sublime (Jan 21 2021 at 00:09):

Suppose I have code like

universe l
structure Thing : Type (l + 1) :=
(Obj : Type l)
(Arr : Obj → Obj → Type l)
(id : ∀ {a} , Arr a a)

variables (A  B : Thing) (f : A.Obj -> B.Obj)

def foo : ∀ a, B.Arr (f a) (f a)
:= λ a, let bid := B.id in @bid (f a)


I would like to avoid the let binding, but Lean complains at both @B.id and B.@id. Is there anything I can do?

#### Yakov Pechersky (Jan 21 2021 at 00:14):

def foo : ∀ a, B.Arr (f a) (f a)
:= λ a, Thing.id _


#### Lime Sublime (Jan 21 2021 at 00:16):

EDIT: This was wrong, sorry (I get a "too many arguments" error message when trying that)

#### Reid Barton (Jan 21 2021 at 00:18):

I don't understand why B.id doesn't work, something weird about implicit argument insertion and dot notation? sounds vaguely familiar...

#### Yakov Pechersky (Jan 21 2021 at 00:22):

Does this not work for you @Lime Sublime ?

universe l
structure Thing : Type (l + 1) :=
(Obj : Type l)
(Arr : Obj → Obj → Type l)
(id : ∀ {a} , Arr a a)

variables (A  B : Thing) (f : A.Obj -> B.Obj)

def foo : ∀ a, B.Arr (f a) (f a)
:= λ a, Thing.id _

#check foo A B f


#### Lime Sublime (Jan 21 2021 at 00:33):

That code works for me! Unfortunately, the solution produces an error in a larger section of code. Trying to build a repro now

#### Reid Barton (Jan 21 2021 at 00:34):

If you need to give an explicit argument for some reason then another option is @Thing.id B (f a)

#### Lime Sublime (Jan 21 2021 at 00:36):

In fact it does work, @Yakov Pechersky ! Thanks! How did you generate the fix?

#### Yakov Pechersky (Jan 21 2021 at 00:37):

I took Reid's suggestion from earlier for the notation to just use the structure's field instead of relying on projection notation

#### Floris van Doorn (Jan 21 2021 at 05:06):

Yeah, you cannot combine the @ with the projection notation (dot notation), so in that case you have to just write the full name of the projection.

Last updated: May 13 2021 at 22:15 UTC