Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Pretty-printing terms without syntactic sugar

Email Gateway (Nov 06 2025 at 15:01):

From: Peter <cl-isabelle-users@lists.cam.ac.uk>
Dear list,

is there a simple way to pretty-print a term without any syntactic sugar
(except basic lambda %_._ and application f x ). Ideally in an
accessible way for beginners.

For example, "{# x∈#S. x<5 #}" should be printed as "filter_mset (λx.
less x 5) S" and "{ x∈S. x<5 }" as "Collect (λx. x∈S ∧ less x 5)"

The only way I know to get a rough impression is to use

ML_val ‹\<^term>‹Collect (λx. x∈S ∧ less x 5)››

but the output is pretty much unreadable.

Background:

• I'm explaining that there is a lot of syntactic sugar, but I don't
  know what to tell students that want to know how certain syntactic sugar
  is actually translated.

• Also, it's sometimes important to know what constants your term
  comprises, e.g., to use find_theorems effectively, or to know what
  definitions to unfold.

--

Peter

Email Gateway (Nov 06 2025 at 18:48):

From: Manuel Eberl <manuel@pruvisto.org>
I think I asked that question already a few years ago, and I once tried
building a command that does this but didn't get very far.

Of course, the question is what you mean by "no syntactic sugar". Even
in your example, you still had "∈" and "∧" as syntax in the output.
Printing numerals without syntactic sugar will also lead to a lot of
clutter.

Note however that since the last release (I think) you can actually
ctrl+click on any notation and it will take you to the place where it
was defined.

Manuel

On 06/11/2025 15:38, Peter (via cl-isabelle-users Mailing List) wrote:

Dear list,

is there a simple way to pretty-print a term without any syntactic
sugar (except basic lambda %_._ and application f x ). Ideally in an
accessible way for beginners.

For example, "{# x∈#S. x<5 #}" should be printed as "filter_mset (λx.
less x 5) S" and "{ x∈S. x<5 }" as "Collect (λx. x∈S ∧ less x 5)"

The only way I know to get a rough impression is to use

ML_val ‹\<^term>‹Collect (λx. x∈S ∧ less x 5)››

but the output is pretty much unreadable.

Background:

• I'm explaining that there is a lot of syntactic sugar, but I don't
  know what to tell students that want to know how certain syntactic
  sugar is actually translated.

• Also, it's sometimes important to know what constants your term
  comprises, e.g., to use find_theorems effectively, or to know what
  definitions to unfold.

--

Peter

Email Gateway (Nov 06 2025 at 19:24):

From: Makarius <makarius@sketis.net>
On 06/11/2025 19:47, Manuel Eberl wrote:

Note however that since the last release (I think) you can actually ctrl+click
on any notation and it will take you to the place where it was defined.

Yes, see this NEWS entry from Isabelle2025:

• Blocks in mixfix annotations now support properties "open_block"
  (bool) and "notation" (string as cartouche). When "open_block" is
  enabled, the block has no impact on formatting, but it may carry markup
  information via "notation". The latter uses formal kinds (e.g. "mixfix",
  "infix", "binder") together with informal words to describe the
  notation. This markup affects both parsing and printing --- it can be
  explored via mouse hovering in the Prover IDE, or programmatically by
  Isabelle/Scala tools. Markup for "infix" and "binder" declarations are
  automatic, but general mixfix forms require manual annotations in the
  theory library. Plenty of existing examples may be found in the Isabelle
  sources by searching for "notation=" (without quotes and no extra
  space). Occasional INCOMPATIBILITY for 'no_syntax' or 'no_notation'
  declarations in user applications: the mixfix template needs to be
  adapted accordingly, but it is often better to use "unbundle no
  foobar_syntax", as explained for HOL libraries below.

That might be a bit too much text, which also needs to be understood in the
greater context of other inner-syntax changes in that release.

The short story:

* infix and binder syntax get notation markup automatically
* free-form mixfix syntax needs markup provided by the author of the theory
library

I've done a lot of such annotations for basic Isabelle/HOL libraries already,
but there is plenty of room for further improvements, especially in AFP
library sessions.

Makarius

Last updated: Nov 09 2025 at 20:21 UTC