Re: [isabelle] translations and numerals




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.