λleanlab

Programs

Parsing with error messages

Use Except and do to return a value or an explanation of failure.

Open Parsing.lean in editor
def parseNumber (text : String) : Except String Nat :=
  match text.toNat? with
  | some n => .ok n
  | none => .error s!"Not a natural number: {text}"

def addText (a b : String) : Except String Nat := do
  let x ← parseNumber a
  let y ← parseNumber b
  return x + y

def describe (result : Except String Nat) : String :=
  match result with
  | .ok n => s!"Sum: {n}"
  | .error message => message

def main : IO Unit := do
  IO.println (describe (addText "20" "22"))
  IO.println (describe (addText "twenty" "22"))

Explanation

Except String Nat

Contains either .ok with a natural number or .error with an error string.

let x ← parseNumber a

In an Except do block, extracts a successful result. An error ends the computation and propagates automatically.

.ok · .error

Constructor names inferred from the expected type. Matching handles both outcomes explicitly.

Expected output

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

Sum: 42
Not a natural number: twenty

Exercise

Reject the number zero with a separate error message.

Related examples