Re: [isabelle] New error messages in Isabelle 2013

On Wed, 30 Jan 2013, Gottfried Barrow wrote:

I put in "declare[[show_types=false]] declare[[show_sorts=false]]", and I didn't see anything extra, but I'll experiment with changing "show_types" back and forth and see what happens.

So lets take my favourite example:

  term "x = x"

Here we ask the system to accept a given term formally, and produce formal output and markup. The output is the tip of the iceberg that you see directly, the markup is what you explore by other means, such
color schemes, formal tooltips etc.

Note that markup is both attached to the input you give and the output that the system produces, but not in a fully symmetric manner.

So the above will give you information about the type of variable x, which is 'a, and its sort, which is "type". You can hover over the "type" to have the system explain to you that it is in fact class "HOL.type", and then you jump to its definition following the implicit hyperlink.

This means you can explore that recursively by hovering over formal input and output -- this is now mostly uniform in Isabelle2013. This unfolds a massive tree of information, or rather a large forest, by walking a few steps into some of its paths.

Instead, if you say:

  declare [[show_types, show_sorts]]
  term "x = x"

the system will interpret this as insisting in the old way: partial annotations for some of the term positions. There is no markup, so you can't explore the types, sorts.

Of course, there are endless possibilities to refine this further. An obvious question is: What is a succinct "digest" (as output text) to give you a types / sorts environment for some formal output. Old show_types / show_sorts are traditionally very crude here. This is only a starting point for further reworking of these ancient mechanisms. In particular, I hope to see certain improvements done for current sledgehammer isar_proofs output to be taken into account as well.


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