*To*: Tobias Nipkow <nipkow at in.tum.de>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] translations and numerals*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 22 Jan 2014 08:07:02 +0100*In-reply-to*: <52DEC92C.7090108@in.tum.de>*References*: <52DE790A.7000902@in.tum.de> <52DE7F25.4000503@gmail.com> <52DE819C.60600@gmail.com> <52DEC92C.7090108@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

Hi Tobias,

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

**Follow-Ups**:**Re: [isabelle] translations and numerals***From:*Tobias Nipkow

**References**:**[isabelle] translations and numerals***From:*Tobias Nipkow

**Re: [isabelle] translations and numerals***From:*Christian Sternagel

**Re: [isabelle] translations and numerals***From:*Christian Sternagel

**Re: [isabelle] translations and numerals***From:*Tobias Nipkow

- Previous by Date: [isabelle] Fool Proof
- Next by Date: Re: [isabelle] translations and numerals
- Previous by Thread: Re: [isabelle] translations and numerals
- Next by Thread: Re: [isabelle] translations and numerals
- Cl-isabelle-users January 2014 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