Operator precedence in heap lang is wrong
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
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.