Re: [isabelle] datatype display problem of type_synonym



Am 17/07/2012 09:29, schrieb Ramana Kumar:
> 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?

Yes.

Tobias

>>
>> 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.