Agda-2.3.2.2: src/rts/RTN.agda

module RTN where

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

  {-# BUILTIN NATURAL Nat #-}
  {-# BUILTIN SUC suc #-}
  {-# BUILTIN ZERO zero #-}