> module A

> public export n : Nat
> n = ?lala