Re: [isabelle] Odd Syntax in HOL/IMP/Natural.thy

"a s" belongs together - it is an application.


George Karabotsos wrote:

I am reading the HOL/IMP theories and I have some difficulty understanding how the following definitions:

update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900)
 "update == fun_upd"

syntax (xsymbols)
update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ \<mapsto> /_]" [900,0,0] 900)

allow for the following syntax:

s[x\<mapsto>a s]
My difficulty lies with understanding how the last instance of <s> (singled out by the ^ symbol) can exist there? When there are three argument placeholders in the syntax statement.

Can someone please point out my misunderstanding?


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