Bool ::= False | True Nat ::= O | S Nat Maybe a ::= Nothing | Just a Not :: Bool -> Bool Not = False -> True | True -> False Match :: _ -> _ -> Bool Match a = a -> True | _ -> False Pred ::= S (x : Nat) -> x