aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/onlyprinting.v
blob: 1973385a0a3886a222703a2705be9f315ed73c23 (plain)
1
2
3
4
5
Reserved Notation "x :-) y" (at level 50, only printing).

Notation "x :-) y" := (plus x y).

Check 0 + 0.