OpenInMutual.agda

-- Currently open declarations are not allowed in mutual blocks.
-- This might change.
module OpenInMutual where

module A where

mutual
  open A
  T : Set -> Set
  T A = A