packages feed

Agda-2.3.2.2: test/succeed/Using.agda

module Using where

module Dummy where
  data DummySet1 : Set where ds1 : DummySet1
  data DummySet2 : Set where ds2 : DummySet2

open Dummy
  using (DummySet1)

open Dummy -- checking that newline + comment is allowed before "using"
  using (DummySet2)