Re: [isabelle] Unwanted type annotations



On Thu, May 16, 2013 at 2:32 PM, Peter Lammich <lammich at in.tum.de> 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.