Zulip Chat Archive

Stream: general

Topic: explicit/implicit switch


view this post on Zulip Patrick Massot (Jun 09 2018 at 09:32):

We have a section where all definitions and lemmas start with either (A : type) [class1 A] [class2 A] [class3 A] [class4 A] or {A : type} [class1 A] [class2 A] [class3 A] [class4 A] ( only difference is () vs {} in first argument). Is there any way we could tell Lean which one we want for each def/lemma without having to copy the whole line or use a different variable name? Of course simply writing (A : Type) or {A : Type} at the beginning of a def doesn't work since it shadows the variable and loses the instance implicit stuff

view this post on Zulip Sebastian Ullrich (Jun 09 2018 at 12:18):

variable {A} changes the binder of an existing variable A

view this post on Zulip Patrick Massot (Jun 09 2018 at 12:51):

Thanks!


Last updated: May 08 2021 at 04:14 UTC