Zulip Chat Archive

Stream: general

Topic: using @ with expressions that are not definitions


Chris Hughes (Jan 12 2022 at 13:07):

Is there a way to get this to work nicely

constant F : Type

constant F_to_fun (f : F) : Π {X : Type}, X  X

example (f : F) (h : (Π (X : Type), X  X)  ) :  :=
h (F_to_fun f)

There is nowhere I can put an @ to make the type of F_to_fun f into Π (X : Type), X → X instead of ?m_1 -> ?m_1

Alex J. Best (Jan 12 2022 at 13:11):

Maybe I'm misunderstanding the question but

constant F : Type

constant F_to_fun (f : F) : Π {X : Type}, X  X

noncomputable
example (f : F) (h : (Π (X : Type), X  X)  ) :  :=
h (@F_to_fun f)

checks fine for me

Chris Hughes (Jan 12 2022 at 13:26):

Thanks. That didn't work in my other example because F_to_fun had some other implicit arguments, but some extra underscores fixed that. I was also confused by the squiggly lines telly me _example was noncomputable, I should have actually read the error.


Last updated: Dec 20 2023 at 11:08 UTC