Local definitions

Local definitions are introduced with the let construct.

import Stdlib.Prelude open;

sum (lst : List Nat) : Nat :=
  let
    go (acc : Nat) : List Nat -> Nat
      | nil := acc
      | (x :: xs) := go (acc + x) xs;
  in go 0 lst;

The declarations within a let statement share the same syntax as those inside a module. However, their visibility is limited to the expression that follows the in keyword.