git.iko.soy/Idris-dev
on master help sign in
Better test for @-_-desugaring
48fd842David Raymond Christiansen
test/sugar005/As.idr+9
compare with master
unifiedsplit
@@ -16,6 +16,12 @@ isSS : Nat -> Maybe (Nat, Nat)
16isSS n@(S m@(S _)) = Just (n,m)
16isSS n@(S m@(S _)) = Just (n,m)
17isSS _ = Nothing
17isSS _ = Nothing
18
18
19+-- Test two @-patterns
20+same : Nat -> Nat -> Maybe Nat
21+same x@(S _) y@(S _) = Just $ x + y
22+same Z Z = Just 42
23+same _ _ = Nothing
24+
19namespace Main
25namespace Main
20 main : IO ()
26 main : IO ()
21 main = do print $ isS 0
27 main = do print $ isS 0
@@ -24,4 +30,7 @@ namespace Main
24 print $ hasS [0,1,2]
30 print $ hasS [0,1,2]
25 print $ isSS 5
31 print $ isSS 5
26 print $ isSS 0
32 print $ isSS 0
33+ print $ same 1 1
34+ print $ same 0 0
35+ print $ same 1 0
27
36
test/sugar005/expected+3
@@ -4,3 +4,6 @@ Nothing
4Just 1
4Just 1
5Just (5, 4)
5Just (5, 4)
6Nothing
6Nothing
7+Just 2
8+Just 42
9+Nothing