binding power

Stream: new members

[Alex Zhang]

If the binding powers are not specified, what is the precedence of :: and ++ in the following examples?

namespace hidden

inductive list (α : Type*)
| nil {} : list
| cons : α → list → list

namespace list

notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l

variable {α : Type*}

notation h :: t  := cons h t

@[simp]
def append (s t : list α) : list α :=
list.rec_on s t (λ x l u, x::u)

notation s ++ t := append s t

[Floris van Doorn]

See https://github.com/leanprover-community/lean/blob/master/library/init/core.lean#L80-L81
It is reserved notation.

reserve infixl ` ++ `:65 -- has_append.append
reserve infixr ` :: `:67 -- list.cons