Email Gateway (Aug 19 2022 at 16:30): Email Gateway (Aug 19 2022 at 16:30):From: mahmoud abdelazim <m.abdelazim@icloud.com>
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
Email Gateway (Aug 19 2022 at 16:30):From: Peter Lammich <lammich@in.tum.de>
"(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
Last updated: Apr 18 2024 at 20:16 UTC