def
definition
def or abbrev
previewNatArray
show as:
view Lean formalization →
formal statement (Lean)
44def previewNatArray (arr : Array Nat) (limit : Nat := 4) : String :=
proof body
Definition body.
45 let previewVals := (arr.toList.take limit).map (fun n => toString n)
46 let body := String.intercalate ", " previewVals
47 if previewVals.isEmpty then "[]"
48 else
49 let ellipsis := if arr.size > previewVals.length then ", …" else ""
50 "[" ++ body ++ ellipsis ++ "]"
51