module Test2 where

open import Test

-- Testing the inter-file goto facility.

test : ℕ
test =  +  + 

-- Testing qualified names.

Eq = Test.Equiv {Test.ℕ}