Agda-2.3.2.2: test/fail/Issue260b.err
Issue260b.agda:5,8-9 Duplicate definition of module R. Previous definition of module R at Issue260b.agda:4,8-9 when scope checking the declaration record R where
Issue260b.agda:5,8-9 Duplicate definition of module R. Previous definition of module R at Issue260b.agda:4,8-9 when scope checking the declaration record R where