agda/examples/outdated-and-incorrect/Alonzo/RTN.agda

module RTN where

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

  {-# BUILTIN NATURAL Nat #-}