idris-0.10.1: test/basic009/A.idr

module A

public export
num : Nat
num = 0