Re: [isabelle] Unwanted type annotations



I think this behaviour is hard-coded into the pretty-printer. On
numerals with variable types, it always prints the type.

Peter


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.