on 385dcbf help sign in
5 lines 44 B history raw
1module B.C
3public export
4num : Nat
5num = 1