module Naturals where

open import Logic

data  : Set where 
     O :               
     succ :          


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