aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/onlyprinting.v
blob: 91a628d792df9d43febffe65015ebb722dd97db7 (plain)
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).