module Naturals where

open import Logic

data ℕ : Set where
     O : ℕ
     succ : ℕ → ℕ


{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO O #-}
{-# BUILTIN SUC succ #-}