# Re: [isabelle] translations and numerals

```Hi Tobias,

```
here's just another data point. In Isabelle2013-2, your original translation works fine with ProofGeneral 3.7.1.1, but not with jEdit. I haven't tried PG 4.x.
```
Andreas

On 21/01/14 20:23, Tobias Nipkow wrote:
```
```

On 21/01/2014 15:18, Christian Sternagel wrote:
```
```Well, what I wrote in my previous mail does not work for "int"s and "nat"s. The
following does

translations
"i" <= "CONST Fin (i::'a::numeral)"
"i" <= "CONST Fin (i::int)"
```
```
But this causes "Fin x" to be reduced to "x", no matter what "x" is, as long as
it is of type int. That's not what I want.

Tobias

```
```   "i" <= "CONST Fin (i::nat)"
"0" <= "CONST Fin (0::'a::zero)"
"1" <= "CONST Fin (1::'a::one)"

But I should mention that I have no clue why ;)... I was just doing trial and
error.

cheers

chris

On 01/21/2014 03:07 PM, Christian Sternagel wrote:
```
```Dear Tobias,

how about (I used "datatype 'a fin = Fin 'a"),

translations
"_Numeral i" <= "CONST Fin (i::'a::numeral)"
"0" <= "CONST Fin (0::'a::zero)"
"1" <= "CONST Fin (1::'a::one)"

then for

term "(Fin 0, Fin 1, Fin 10, Fin x)"

I get

"(0, 1, 10, Fin x)"
:: "'a fin × 'b fin × 'c fin × 'd fin"

Note that when leaving of "zero" and "one I get "Fin 0" and "Fin 1" as
output.

On 01/21/2014 02:41 PM, Tobias Nipkow wrote:
```
```I am using Library/Extended that defines a datatype with a unary
constructor
Fin. I want to print terms like "Fin 5" as "5" and am using the following
translations:

translations
"_Numeral i" <= "CONST Fin(_Numeral i)"
"0" <= "CONST Fin 0"
"1" <= "CONST Fin 1"

When I generate latex from

text{* @{term "Fin(5::int)"} *}

this works fine, I get "5".

But when I write

term "Fin(5::int)"

in a theory, the output is "Fin 5". Why is that? And what can I do to
obtain the
output "5" always, not just from an antiquotation in a text block.

Note that when I use this translation

translations
"x" <= "CONST Fin(x)"

then "Fin" disappears for good, but that is not what I want.

Thanks
Tobias

```
```
```
```

```

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