Agda-2.3.2.2: test/succeed/TopLevelImport.agda

import Nat
open   Nat using (Nat)

module TopLevelImport (n : Nat) where

  it : Nat
  it = n