on master help sign in
add test cases verifying new verbatim string behavior
5fd758cMichael Morgan
test/primitives003/expected+4
@@ -5,6 +5,10 @@ False
5True
5True
6False
6False
7True
7True
8+True
9+True
10+True
11+True
8False
12False
9True
13True
10False
14False
test/primitives003/test038.idr+14−10
@@ -1,4 +1,4 @@
1−module Main
1+module Main
2
2
3import Data.Vect
3import Data.Vect
4import Data.Fin
4import Data.Fin
@@ -17,18 +17,22 @@ main = do
17 putStrLn . show $ test "hello" "world"
17 putStrLn . show $ test "hello" "world"
18 putStrLn . show $ test (the Char '\0') (the Char '\0')
18 putStrLn . show $ test (the Char '\0') (the Char '\0')
19 putStrLn . show $ test (the Char '\1') (the Char '\2')
19 putStrLn . show $ test (the Char '\1') (the Char '\2')
20+ putStrLn . show $ test """""" ""
21+ putStrLn . show $ test """"hello"""" "\"hello\""
22+ putStrLn . show $ test """""hello""""" "\"\"hello\"\""
23+ putStrLn . show $ test """""""""" "\"\"\"\""
20-- Non-primitives
24-- Non-primitives
21 -- Vect
25 -- Vect
22− putStrLn . show $
26+ putStrLn . show $
23 test (the (Vect _ Int) [1,2,3]) (the (Vect _ Int) [1,2,3])
27 test (the (Vect _ Int) [1,2,3]) (the (Vect _ Int) [1,2,3])
24− putStrLn . show $
28+ putStrLn . show $
25 test (the (Vect _ Int) [1,2,3]) (the (Vect _ Int) [1,2,4])
29 test (the (Vect _ Int) [1,2,3]) (the (Vect _ Int) [1,2,4])
26 -- List
30 -- List
27− putStrLn . show $
31+ putStrLn . show $
28 test (the (List Int) [1,2,3]) (the (List Int) [1,2,3])
32 test (the (List Int) [1,2,3]) (the (List Int) [1,2,3])
29− putStrLn . show $
33+ putStrLn . show $
30 test (the (List Int) [1,2,3]) (the (List Int) [1,2])
34 test (the (List Int) [1,2,3]) (the (List Int) [1,2])
31− putStrLn . show $
35+ putStrLn . show $
32 test (the (List Int) [1,2,3]) (the (List Int) [1,2,4])
36 test (the (List Int) [1,2,3]) (the (List Int) [1,2,4])
33 -- Tuple
37 -- Tuple
34 putStrLn . show $
38 putStrLn . show $
@@ -45,16 +49,16 @@ main = do
45 putStrLn . show $ test (Just "hello") (Just "world")
49 putStrLn . show $ test (Just "hello") (Just "world")
46 putStrLn . show $ test (Just "hello") Nothing
50 putStrLn . show $ test (Just "hello") Nothing
47 -- Either
51 -- Either
48− putStrLn . show $ test (the (Either String Bool) (Left "hello"))
52+ putStrLn . show $ test (the (Either String Bool) (Left "hello"))
49 (the (Either String Bool) (Left "hello"))
53 (the (Either String Bool) (Left "hello"))
50− putStrLn . show $ test (the (Either String Bool) (Left "hello"))
54+ putStrLn . show $ test (the (Either String Bool) (Left "hello"))
51 (the (Either String Bool) (Left "world"))
55 (the (Either String Bool) (Left "world"))
52 putStrLn . show $ test (Left "hello") (Right "world")
56 putStrLn . show $ test (Left "hello") (Right "world")
53 putStrLn . show $ test (Left "hello") (Right False)
57 putStrLn . show $ test (Left "hello") (Right False)
54 -- Fin
58 -- Fin
55− putStrLn . show $ test (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))
59+ putStrLn . show $ test (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))
56 (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))
60 (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))
57− putStrLn . show $ test (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))
61+ putStrLn . show $ test (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))
58 (the (Fin (S (S (S (Z))))) (FS (FZ)))
62 (the (Fin (S (S (S (Z))))) (FS (FZ)))
59 -- Nat
63 -- Nat
60 putStrLn . show $ test (S (S (S Z))) (S (S (S Z)))
64 putStrLn . show $ test (S (S (S Z))) (S (S (S Z)))