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