implicit instance arguments — Mathlib

Lean4

/-- There are places where typeclass arguments are specified with implicit `{}` brackets instead of
the usual `[]` brackets. This is done when the instances can be inferred because they are implicit
arguments to the type of one of the other arguments. When they can be inferred from these other
arguments, it is faster to use this method than to use type class inference.

For example, when writing lemmas about `(f : α →+* β)`, it is faster to specify the fact that `α`
and `β` are `Semiring`s as `{rα : Semiring α} {rβ : Semiring β}` rather than the usual
`[Semiring α] [Semiring β]`.
-/
def «implicit instance arguments» : LibraryNote✝ :=
  ()

Похожие утверждения