on master help sign in
fixed name of module, renaming from my private module name to the correct name for addition in prelude
71705d5Dominic Mulligan
lib/prelude/nat.idr+1−1
@@ -1,4 +1,4 @@
1−module MoreNat
1+module prelude.nat
2
2
3import builtins
3import builtins
4
4