Agda-2.3.2.2: examples/outdated-and-incorrect/Alonzo/RTN.agda

module RTN where

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

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