test-suite/output/bug_13112.v


1
2
3
4
5

Reserved Notation "'HI'".
Notation "'HI'" := (O + O) (only parsing).
Check HI. (* 0 + 0 : nat *)
Notation "'HI'" := (O + O) (only printing).
Check HI. (* 0 + 0 : nat *)