# [isabelle] Defining {x} == {x, x} using "syntax", "translations", & one function

```Hi,

```
I'm trying to define the singleton "{x} == {x,x}", as shown on line 90 of the attached screenshot. I've tried lots of different things, but I have the following four lines, :
```
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)

```
QUESTION: Can I somehow get "{x} == {x,x}" using only "syntax", "translations", and the one function "upS"? I'm trying not to introduce a second function.
```
*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"

```
So this last example shows me a simple way to get what I'm trying to do, but, at least at this point, I'd rather not introduce another function.
```
Thanks,
GB

```

Attachment: singleton_def_error.png
Description: PNG image

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