test-suite/success/onlyprinting.v


1
2
3
4
5
6
7

Notation "x ++ y" := (plus x y) (only printing).

Fail Check 0 ++ 0.

Notation "x + y" := (max x y) (only printing).

Check (eq_refl : 42 + 18 = 60).