Notation for List literals.

def «term[_]» : Lean.ParserDescr

The syntax [a, b, c] is shorthand for a :: b :: c :: [], or List.cons a (List.cons b (List.cons c List.nil)). It allows conveniently constructing list literals.

For lists of length at least 64, an alternative desugaring strategy is used which uses let bindings as intermediates as in let left := [d, e, f]; a :: b :: c :: left to avoid creating very deep expressions. Note that this changes the order of evaluation, although it should not be observable unless you use side effecting operations like dbg_trace.

Conventions for notations in identifiers:

• The recommended spelling of [] in identifiers is nil.

• The recommended spelling of [a] in identifiers is singleton.

Equations

• One or more equations did not get rendered due to their size.

def «term%[_|_]» : Lean.ParserDescr

Auxiliary syntax for implementing [$elem,*] list literal syntax. The syntax %[a,b,c|tail] constructs a value equivalent to a::b::c::tail. It uses binary partitioning to construct a tree of intermediate let bindings as in let left := [d, e, f]; a :: b :: c :: left to avoid creating very deep expressions.

Equations

• One or more equations did not get rendered due to their size.