Re: [isabelle] Unwanted type annotations



> Do you just don't want to see it as end-user, or does some ML code of yours depend critically on a certain behaviour?

In Sledgehammer, we generate proof texts with a minimal amount of type annotations. The code assumes that only the annotations introduced with Type.constraint will be printed. (Therefore, I refer to any other annotations procuced by the pretty printer as "unwanted").

The example I posted is the first one I encountered for which this assumption does not hold. The "unwanted annotations" do not break the generated Isar-Proof, they just look ugly (and are useless).

-- Steffen

On 17.05.2013, at 17:29, Makarius <makarius at sketis.net> wrote:

> On Thu, 16 May 2013, Steffen Juilf Smolka wrote:
> 
>> 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
> 
> The question is what all these flags mean in detail, also what you mean by "unwanted".  Do you just don't want to see it as end-user, or does some ML code of yours depend critically on a certain behaviour?
> 
> The inner syntax pretty printing infrastructure of Isabelle is very flexible, and many details are determined by translation functions in user space (here the HOL library).
> 
> You can search the Isabelle/HOL sources for the syntax const "_constrain" to get an idea where certain notation takes special care about such extra type constraints.  You can then make educated guesses on which kind of behaviour you can bet, or better not.
> 
> 
> 	Makarius





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