*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] translations and numerals*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Tue, 21 Jan 2014 15:18:04 +0100*In-reply-to*: <52DE7F25.4000503@gmail.com>*References*: <52DE790A.7000902@in.tum.de> <52DE7F25.4000503@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

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

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

- Previous by Date: Re: [isabelle] translations and numerals
- Next by Date: [isabelle] returning to the original document in Isabelle/jedit
- 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