Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] syntax translation

Email Gateway (Aug 19 2022 at 09:15):

From: li yongjian <lyj238@gmail.com>
Dear expert:
I want to define a syntax abbreaviation as follows:
In latex source $n1\rightarrow_{SP}n2 \equiv (n1,n2) \in casual SP$
(please see the figures in attachment),

where casual1 is defined as follows:

definition

casual1:: "strand_space \<Rightarrow>( node \<times> node ) set " where
"casual1 SP \<equiv> { (n1,n2) . n1 \<in> Domain SP \<and> n2 \<in>
Domain SP \<and>
node_sign SP n1= + \<and>
node_sign SP n2= -
\<and> node_term SP n1= node_term SP n2
\<and> strand n1 \<noteq> strand n2
} "

I have tried the following code, however, it cannot pass, can you
give me a hand?
syntax
"_casual1"::" [node,strand_space,node]\<Rightarrow>bool" (
"_\<rightarrow>_/ _" )

translations
"n1\<rightarrow>SP n2" == "CONST member (n1,n2) (casual1 SP)"

regards
lyj
syntax.png

Email Gateway (Aug 19 2022 at 09:15):

From: Tobias Nipkow <nipkow@in.tum.de>
If I replace "node", "strand_space", "member" and "casual" (which I don't have)
and just define

syntax
"_casual1" :: " ['a,'b,'a]\<Rightarrow>bool" ("_\<rightarrow>_/ _")

translations
"n1\<rightarrow>SP n2" == "(n1,n2) : SP"

it works fine for me.

Tobias

Email Gateway (Aug 19 2022 at 09:15):

From: Lars Noschinski <noschinl@in.tum.de>
On 29.11.2012 08:00, Tobias Nipkow wrote:

Dear expert:
I want to define a syntax abbreaviation as follows:
In latex source $n1\rightarrow_{SP}n2 \equiv (n1,n2) \in casual SP$
(please see the figures in attachment),
[...]
If I replace "node", "strand_space", "member" and "casual" (which I don't have)
and just define

syntax
"_casual1" :: " ['a,'b,'a]\<Rightarrow>bool" ("_\<rightarrow>_/ _")

translations
"n1\<rightarrow>SP n2" == "(n1,n2) : SP"

Actually, what is the advantage of using syntax/translations here
instead of mixfix annotations?

-- Lars

Last updated: Nov 21 2024 at 12:39 UTC