@@ -16,6 +16,12 @@ isSS : Nat -> Maybe (Nat, Nat)
1616isSS n@(S m@(S _)) = Just (n,m)
1717isSS _ = Nothing
1818
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+
1925namespace Main
2026 main : IO ()
2127 main = do print $ isS 0
@@ -24,4 +30,7 @@ namespace Main
2430 print $ hasS [0,1,2]
2531 print $ isSS 5
2632 print $ isSS 0
33+ print $ same 1 1
34+ print $ same 0 0
35+ print $ same 1 0
2736