Re: [isabelle] translations and numerals



Thank you, that explains why the translations worked for me when I wrote them -
I used PG then.

Tobias

On 22/01/2014 08:07, Andreas Lochbihler wrote:
> 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.