Re: [isabelle] Unwanted type annotations

Is there a way to turn this feature off or to predict reliably when annotations are inserted?
From the code it seems that numerals with polymorphic types are annotated, then again i know @{term 1} is polymorhpic but printed without annotation. I guess I don't understand the code completely…

The code I am working on equips terms with a minimal set of type annotations which ensures the types of the terms are preserved (when printing and reparsing the terms).

Thanks for you help!

On 17.05.2013, at 19:32, Brian Huffman <huffman.brian.c at> wrote:

> On Thu, May 16, 2013 at 2:32 PM, Peter Lammich <lammich at> wrote:
>> I think this behaviour is hard-coded into the pretty-printer. On
>> numerals with variable types, it always prints the type.
> Pretty-printing for numerals is implemented with a
> "typed_print_translation (advanced)" command in HOL/Num.thy. The bit
> of ML code there implements the logic for deciding when to add a type
> annotation.
> This is an intentional feature. Without it, a numeral like "0" might
> be parsed with a too-general type like "0::'a::zero" without the
> user's knowledge, leading to much confusion.
> - Brian
>> On Do, 2013-05-16 at 18:41 +0200, Steffen Juilf Smolka wrote:
>>> Hi,
>>> For some reason, I can't get Isabelle to print the following term without type annotations:
>>> val t = @{term "0∷'a∷comm_monoid_add"}
>>> I have tried
>>> val ctxt = @{context}
>>> |> Config.put show_markup                false
>>> |> Config.put show_types                 false
>>> |> Config.put show_free_types            false
>>> |> Config.put show_all_types             false
>>> |> Config.put show_sorts                 false
>>> val _ = t |> Syntax.string_of_term ctxt |> writeln
>>> which produces the output "0∷'a". Am I doing something wrong?
>>> Best Regards,
>>> Steffen

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