Re: [isabelle] translations and numerals
Works like a charm, thanks!
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
>> "_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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and