Check match 2 with 0 => 0 | S n => n end. Notation "|" := 1 (compat "8.4"). Check match 2 with 0 => 0 | S n => n end. (* fails *)