Re: [isabelle] Precedences of map_upd vs. fun_upd

On 29/07/2015 18:45, Andreas Lochbihler wrote:
So if we unify the precedences, which one should be prefered? I am slightly in
favour of those for maps, because they allow you to write "f x(y |-> z)" without

I may seem convenient but it can leave the reader wondering. Hence I prefer the notation that requires parentheses

By the way, why are there different non-terminals for map update and fun update
anyway? AFAICS one could use the same non-terminals for both kinds of function
updates. Then it would be possible to write things like

term "f(a := q, x â y, z := None)"

At the moment, this must be written as "(f(a := q)(x â y))(z := None)".

That makes sense.



On 29/07/15 18:08, Tobias Nipkow wrote:
I don't think there is a master plan at work but more likely an oversight. I
remember any argument against unifying the precedences.


On 29/07/2015 16:54, Andreas Lochbihler wrote:
Dear all,

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]

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

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?


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.