explicit/implicit switch

Stream: general

[Patrick Massot]

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

[Sebastian Ullrich]

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

[Patrick Massot]

Thanks!