Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: Type constraints for constants (inne...

Email Gateway (Oct 16 2024 at 21:26):

From: Makarius <makarius@sketis.net>
* General *

• Inner syntax translations now support formal dependencies via commands
  'syntax_types' or 'syntax_consts'. This is essentially an abstract
  specification of the effect of 'translations' (or translation functions
  in ML). Most Isabelle theories have been adapted accordingly, such that
  hyperlinks work properly e.g. for "['a, 'b] ⇒ 'c" or "⟦A; B⟧ ⟹ C" in
  Pure, and "∀x∈A. B x" or "∃x∈A. B x" in HOL.

This refers to Isabelle/8e7bd0566759.

The key change is Isabelle/26ecbac09941, but it only turned out that simple
due to many "changed for change elimination" before it.

A few more details are still missing, e.g. type constraints for mixfix delimiters.

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Email Gateway (Oct 17 2024 at 09:13):

From: Norbert Schirmer <nschirmer@apple.com>
Hi Makarius,

Thanks a lot for the work.

* General *

• Inner syntax translations now support formal dependencies via commands
  'syntax_types' or 'syntax_consts'. This is essentially an abstract
  specification of the effect of 'translations' (or translation functions
  in ML). Most Isabelle theories have been adapted accordingly, such that
  hyperlinks work properly e.g. for "['a, 'b] ⇒ 'c" or "⟦A; B⟧ ⟹ C" in
  Pure, and "∀x∈A. B x" or "∃x∈A. B x" in HOL.

This refers to Isabelle/8e7bd0566759.

I guess you wanted to mention this News entry:

• Inner syntax printing now supports type constraints for constants:
  this is guarded by the configuration options "show_consts_markup"
  (default true) and "show_markup" (default true for PIDE interaction).
  Ast translation rules (command 'translations') and mixfix notation work
  with or without such extra constraints, but ML translation functions
  (command 'print_ast_translation') need may need to be changed slightly.
  Rare INCOMPATIBILITY. The Prover IDE displays type constraints for
  constants as for variables, e.g. via C-mouse hovering.

The key change is Isabelle/26ecbac09941, but it only turned out that simple due to many "changed for change elimination" before it.

A few more details are still missing, e.g. type constraints for mixfix delimiters.

Looking forward to it.

Regards,
Norbert

--

Norbert Schirmer (nschirmer@apple.com)
 SEG Formal Verification

Email Gateway (Oct 18 2024 at 20:56):

From: Makarius <makarius@sketis.net>
On 17/10/2024 11:12, Norbert Schirmer wrote:

I guess you wanted to mention this News entry:

• Inner syntax printing now supports type constraints for constants:
  this is guarded by the configuration options "show_consts_markup"
  (default true) and "show_markup" (default true for PIDE interaction).
  Ast translation rules (command 'translations') and mixfix notation work
  with or without such extra constraints, but ML translation functions
  (command 'print_ast_translation') need may need to be changed slightly.
  Rare INCOMPATIBILITY. The Prover IDE displays type constraints for
  constants as for variables, e.g. via C-mouse hovering.

You are right. Here is an updated version:

• Inner syntax printing now supports type constraints for constants,
  optionally with mixfix syntax (infix, binder etc.). This is guarded by
  the configuration options "show_consts_markup" (default true) and
  "show_markup" (default true for PIDE interaction). The Prover IDE
  displays type constraints as usual via C-mouse hovering. Ast translation
  rules (command 'translations') already work with extra type constraints,
  but the result omits the type of a matched constant. ML translation
  functions (command 'print_ast_translation') based on Ast.unfold_ast etc.
  work in the same manner, but more complex translations may require
  manual changes: rare INCOMPATIBILITY.

See Isabelle/0e27325da568.

After so many renovations of the inner-syntax engine, old problems get
actually solved, although it has required some decades.

Now the situation is again asymmetric, because mixfix consts don't get type
constraints on input.

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Mar 11 2026 at 20:36 UTC