idris-0.12.3: test/regression002/A.lidr

> module A

> public export n : Nat
> n = ?lala