onlyprinting.v « output « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

path: root/test-suite/output/onlyprinting.v

blob: 1973385a0a3886a222703a2705be9f315ed73c23 (plain)

Reserved Notation "x :-) y" (at level 50, only printing).

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

Check 0 + 0.