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 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.