Re: [isabelle] Array



On Di, 2014-11-25 at 15:48 +0100, mahmoud abdelazim wrote:
> In Isabelle i can do that : 
> (λx. 0) (''x'':= 7,’’z’’:= 4)
> And i want to do the following :
> (λx. 0) (‘’Array'':= (1:=2, 2:=0, 3:=4),’’z’’:= 4)
> but i have problems, how can i  


"(1:=2, 2:=0, 3:=4)" is no valid syntax in isabelle. You have to apply
the function update operator to some function, e.g.,

"(%x. 0)(1:=2, 2:=0, 3:=4)"

Alternatively, you could define your own syntax, 
like the "<''x'':=1, ''y'' := 2>" in IMP/AExp


--
  Peter






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