Re: [isabelle] New error messages in Isabelle 2013
- To: Gottfried Barrow <gottfried.barrow at gmx.com>
- Subject: Re: [isabelle] New error messages in Isabelle 2013
- From: Makarius <makarius at sketis.net>
- Date: Fri, 1 Feb 2013 13:18:41 +0100 (CET)
- Cc: cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <5109C114.firstname.lastname@example.org>
- References: <CAAPnxw0UBFawv0Szb6Mkf73Fodkx0JC5L=q_9LWfPnsmxTtfxA@mail.gmail.com> <alpine.LNX.email@example.com> <CAAPnxw2=cxRrFebQKxFxPGrQpfWvTsLp6uiYuSfrt_4+miQiKw@mail.gmail.com> <alpine.LNX.firstname.lastname@example.org> <CAAPnxw1Tt5QvH4H9yLdsB5fhetgiqChsV+tfxxyrQBUiF+==QQ@mail.gmail.com> <5106B811.email@example.com> <alpine.LNX.firstname.lastname@example.org> <5106E225.email@example.com> <alpine.LNX.firstname.lastname@example.org> <5109C114.email@example.com>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
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