Re: [isabelle] translations and numerals



Works like a charm, thanks!

Tobias

On 22/01/2014 19:03, Makarius wrote:
> On Tue, 21 Jan 2014, 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"
> 
> Printing is a black art, especially when using the AST representation of
> 'translations', which can contain additional annotations unexpectedly.
> 
> The configuration option syntax_ast_trace generally helps to see what happens to
> happen in a particular situation, and it shows additional constraints and markup
> in the rich document output of Isabelle/PIDE.
> 
> In other print modes, there can be different add-ons.
> 
> 
> Instead of these fragile and complicated syntax translations, the usual way to
> modify term output systematically is via the "uncheck" phase. It has the
> advantage that it operates on regular type-correct lambda terms: that requires a
> few more cases to cover (in Isabelle/ML), but there is no black magic.
> 
> The included theory No_Fin demonstrates that.  Note that I am using a fully
> official constant no_Fin here, which is not printed in the end due to its
> special notation.
> 
> 
>     Makarius




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