[isabelle] Precedences of map_upd vs. fun_upd
In Isabelle/HOL, function update has the syntax f(x := y) and map update uses f(x |-> y).
Surprisingly, the syntaxes have different precedences. Function update uses
"_Update" :: ['a, updbinds] => 'a ("_/'((_)')" [1000,0] 900)
and map update uses
"_MapUpd" :: "['a ~=> 'b, maplets] => 'a ~=> 'b" ("_/'(_')" [900,0]900)
Consequently, Isabelle accepts the term "f x(1 |-> 2)", but not "f x(1 := Some 2)". The
latter has to parenthesized as in "(f x)(1 := Some 2)".
Browsing the repository, I found that Tobias added the map syntax in 2003 (d2e550609c40)
and that David von Oheimb has changed the precedences for function update in 2000
(666d3a4f3b9d). Before that, precedences for function update were the same as they are now
Can anyone remember why David changed the precedences and why Tobias used the older
precedences when he introduced the syntax for maps? Why are the precedences not the same?
And should they be unified?
This archive was generated by a fusion of
Pipermail (Mailman edition) and