amohrland

module plfa.part1.Naturals where

data N : Set where
  zero : N
  suc : N -> N

{-# BUILTIN NATURAL N #-}

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)