Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 18 2022 at 10:53):

From: George Karabotsos <g_karab@cs.concordia.ca>
Hello,

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

constdefs
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?

George

Email Gateway (Aug 18 2022 at 10:53):

From: Tobias Nipkow <nipkow@in.tum.de>
"a s" belongs together - it is an application.

Tobias

George Karabotsos wrote:

Last updated: May 03 2024 at 08:18 UTC