λleanlab

Programs

Arrays and bounds

Build an array and access an element with a checked bound.

Open Arrays.lean in editor
def squares (count : Nat) : Array Nat := Id.run do
  let mut result := #[]
  for i in [0:count] do
    result := result.push (i * i)
  return result

def atOr (xs : Array Nat) (i fallback : Nat) : Nat :=
  if h : i < xs.size then
    xs[i]'h
  else
    fallback

def main : IO Unit := do
  let xs := squares 5
  IO.println s!"Squares: {xs.toList}"
  IO.println (atOr xs 3 999)
  IO.println (atOr xs 10 999)

Explanation

Id.run do

Allows do notation and local mutable variables in a pure function.

[0:count]

A range beginning at zero and ending before count.

if h : … · xs[i]'h

Names the condition’s proof in the true branch. The array access uses h to establish that i is in bounds.

Expected output

Reference only. Run the file to check its actual result.

Squares: [0, 1, 4, 9, 16]
9
999

Exercise

Produce cubes instead of squares. Keep the out-of-bounds fallback.

Related examples