Stream: Mirror: Isabelle Development Mailing List

Topic: NEWS: Clarified semantics for adding code equations

Email Gateway (Jun 27 2025 at 06:08):

From: Florian Haftmann <florian.haftmann@cit.tum.de>
In 2865a6618cba the semantics for adding code equations has been
clarified and also (for the first time) documented as such:

• Code equations from preceding theories are superseded.
• Code equations declared in the course of a theory are appended, not
  prepended.

This allows to write down code equations in a »natural« order as you
would expect in a functional programming language.

For the case that an application needs transition, you may use

declare [[code_prepend_allowed]] – ‹vanishes at end of theory›

lemma [code prepend]:
…

to use the former prepend semantics. This is only a device for migration
and will vanish sooner or later.

It is anyway very unlikely that this is actually needed – during the
migration of existing theories it turned out that most code equations
are declared in »natural« order anyway, which now fits perfectly to the
clarified semantics.

Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

Last updated: Jul 12 2025 at 16:25 UTC