Agda-2.3.2.2: test/succeed/Issue138.agda

-- records are allowed in mutual blocks

module Issue138 where

mutual
  B = Set
  record Foo : Set where