Re: [isabelle] Unwanted type annotations

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.


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