Zulip Chat Archive

Stream: general

Topic: Providing implicit arguments to a function field


view this post on Zulip 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?

view this post on Zulip Yakov Pechersky (Jan 21 2021 at 00:14):

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

view this post on Zulip Lime Sublime (Jan 21 2021 at 00:16):

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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Lime Sublime (Jan 21 2021 at 00:36):

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

view this post on Zulip 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

view this post on Zulip 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