Re: [isabelle] datatype display problem of type_synonym



On Tue, Jul 17, 2012 at 8:22 AM, Tobias Nipkow <nipkow at in.tum.de> wrote:
> Type synonyms are expanded during parsing. They beautify the input but cannot
> occur in the output.

In HOL4, the printer attempts to use user-defined type synonyms when
possible, helping increase consistency between input and output.
Sometimes, of course, if you have many synonyms for the same type, you
get the wrong one printed.
Was it a principled decision not to print synonyms in Isabelle?

>
> Tobias
>
> Am 16/07/2012 12:25, schrieb chunhan wu:
>> Hi,
>>
>> I tried the following:
>>
>> type_synonym my_int = int
>>
>>    text {* @{typ my_int} *}
>>
>>    datatype foo = A | B my_int
>>
>>    text {* @{datatype foo} *}
>>
>> The "text" works and prints out "my_int",
>> but the "datatype" prints out "int"
>> which should be "my_int".
>>
>> Is there an attribute for datatype antiquotation
>> to solve this problem?
>>
>> Regards,
>>
>> Chunhan
>>
>
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.