Local definitions

Local definitions are introduced with the let construct.

open import Stdlib.Prelude;

sum : List Nat -> Nat;
sum lst :=
  let
    go : Nat -> List Nat -> Nat;
    go acc nnil := acc;
    go acc (x :: xs) := go (acc + x) xs;
  in go zero 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.

Comments