GitLab

The Iris version is dev.2020-05-18.2.fdda97e8.

Given the definition

Definition v: expr := #true || #false = #false.

I expect it to read the same as in most other languages: "Either true is true or false is equal to false". However, Print v shows:

v = ((if: #true then #true else #false) = #false)%E
     : expr

In other words, || has higher precedence than comparisons. I'm not familiar with how exactly notations in Coq are specified, but, looking at notation.v, it seems that precedence for common operators is not specified explicitly but is instead inherited from other notations that are known to Coq, and in vanilla Coq = has low precedence, given its role.