*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] translations and numerals*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 21 Jan 2014 20:23:24 +0100*In-reply-to*: <52DE819C.60600@gmail.com>*References*: <52DE790A.7000902@in.tum.de> <52DE7F25.4000503@gmail.com> <52DE819C.60600@gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

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:*Andreas Lochbihler

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

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

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

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