Agda Template

Remix this to get started with Agda (v2.6.0.1).

module LearnYouAn where

  data ℕ : Set where
    zero : ℕ
    suc : ℕ → ℕ

  _+_ : ℕ → ℕ → ℕ
  zero + m = m
  (suc n) + m = suc (n + m)