PragmaInMutual.agda

-- Currently pragmas are not allowed in mutual blocks.
-- This might change.
module PragmaInMutual where

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

mutual
  {-# BUILTIN NATURAL Nat #-}
  T : Set -> Set
  T A = A