*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Defining {x} == {x, x} using "syntax", "translations", & one function*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Thu, 23 Aug 2012 14:59:44 -0500*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Hi,

consts upS :: "??e?t ? ??e?t ? ??e?t" syntax "_upS" :: "args ? ??e?t" ("{_}??") translations "{u,v}??" == "CONST upS u v" translations "{u}??" == "{u,u}??" On the fourth line above, I get this error: Error in syntax translation rule: duplicate vars in lhs ("_upS" ("_args" u u)) -> ("_upS" u)

*EXAMPLES I'VE LOOKED AT* *src/ZF/ZF.thy line 141:* translations .... "<x, y, z>" == "<x, <y, z>>" "<x, y>" == "CONST Pair(x, y)" *src/HOL/Set.thy line 140:* syntax "_Finset" :: "args => 'a set" ("{(_)}") translations "{x, xs}" == "CONST insert x {xs}" "{x}" == "CONST insert x {}" *src/HOL/ZF/HOLZF.thy:* definition Singleton:: "ZF \<Rightarrow> ZF" where "Singleton x == Upair x x"

Thanks, GB

**Attachment:
singleton_def_error.png**

**Follow-Ups**:**Re: [isabelle] Defining {x} == {x, x} using "syntax", "translations", & one function***From:*Gottfried Barrow

- Previous by Date: Re: [isabelle] Reports like command/ctrl‑mouse‑hover in Output pan?
- Next by Date: Re: [isabelle] Defining {x} == {x, x} using "syntax", "translations", & one function
- Previous by Thread: Re: [isabelle] Is Isabelle/Pure really a meta-logic?
- Next by Thread: Re: [isabelle] Defining {x} == {x, x} using "syntax", "translations", & one function
- Cl-isabelle-users August 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list