mathlib
201a3f4a - chore(*): remove extra parentheses in universe annotations (#14595)

Commit
3 years ago
chore(*): remove extra parentheses in universe annotations (#14595) We change `f.{(max u v)}` to `f.{max u v}` throughout, and similarly for `imax`. This is for consistency with the rest of the code. Note that `max` and `imax` take an arbitrary number of parameters, so if anyone wants to add a second universe parameter, they'll have to add the parentheses again.
Author
Parents
Loading