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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.