Re: [isabelle] datatype display problem of type_synonym



Type synonyms are expanded during parsing. They beautify the input but cannot
occur in the output.

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.