Recursion principle

In type theory, the recursor or recursion principle of a type defines simple pattern matching for that type. Recursors are the non-dependent special cases of induction principles.

Example

â„•

  data â„• : Type where
    Z : â„•
    S : ℕ → ℕ

  ℕ-rec : ∀ r → r → (ℕ → r → r) → ℕ → r

  fac : ℕ → ℕ
  fac = ℕ-rec ℕ 1 (λ n p → n * p)

References