1type family (x :: N) + (y :: N) :: N where
2  'Zero + y = y
3  'Succ n + y = 'Succ (n + y)
4
5type family (x :: N) `LEQ` (y :: N) :: Bool where
6  'Zero `LEQ` y = 'True
7  'Succ n `LEQ` 'Zero = 'False
8  'Succ n `LEQ` 'Succ m = n `LEQ` m
9
10type family ((x :: N) `Weird` (y :: N)) (z :: N) :: Bool where
11  'Zero `Weird` 'Zero 'Zero = 'True
12