Zulip Chat Archive

Stream: new members

Topic: binding power


Alex Zhang (Jun 17 2021 at 04:12):

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 (Jun 17 2021 at 05:16):

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

Last updated: Dec 20 2023 at 11:08 UTC