idris-0.10.1: test/basic009/B/C.idr

module B.C

public export
num : Nat
num = 1