module Lib.Nat where

data Nat : Set where
  zero : Nat
  suc : Nat → Nat
{-# BUILTIN NATURAL Nat #-}

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

data Fin : Nat → Set where
  zero : ∀ { n } → Fin (suc n)
  suc : ∀ { n } → (i : Fin n) → Fin (suc n)