git.iko.soy/Idris-dev
on master help sign in
Change Show instance for Nat to show integers
commitd8580163a1541ec6e326ebd931a7c84b4483070d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 28 Jun 2013, 17:24 (13 years ago) parent7af449c
6 files changed+9−10
compare with master
unifiedsplit
lib/Prelude.idr+3−4 test/reg004/expected+2−2 test/reg017/expected+1−1 test/test005/expected+1−1 test/test007/expected+1−1 test/test019/expected+1−1
lib/Prelude.idr+3−4
@@ -24,10 +24,6 @@ import Prelude.Chars
2424class Show a where
2525 show : a -> String
2626
27−instance Show Nat where
28− show O = "O"
29− show (S k) = "s" ++ show k
30−
3127instance Show Int where
3228 show = prim__toStrInt
3329
@@ -43,6 +39,9 @@ instance Show Char where
4339instance Show String where
4440 show = id
4541
42+instance Show Nat where
43+ show n = show (the Integer (cast n))
44+
4645instance Show Bool where
4746 show True = "True"
4847 show False = "False"
test/reg004/expected+2−2
@@ -1,2 +1,2 @@
1−O
2−sO
1+0
2+1
test/reg017/expected+1−1
@@ -1 +1 @@
1−ssssO
1+4
test/test005/expected+1−1
@@ -1,5 +1,5 @@
118
2−sO
2+1
33(abc, 123)
44(abc, 123)
55([1, 2], [3, 4, 5])
test/test007/expected+1−1
@@ -1,4 +1,4 @@
11Just 8
2−Just sssssssssO
2+Just 9
33Just 42
44Nothing
test/test019/expected+1−1
@@ -1 +1 @@
1−sO
1+1