1 2 3 4 5 6 7 8 9
(* Non exhaustive pattern-matching *) Fail Check (fun x => match x, x with | O, S (S y) => true | O, S x => false | S y, O => true end).