Stream: Mirror: Isabelle Development Mailing List

Topic: NEWS


view this post on Zulip Email Gateway (Jan 10 2026 at 08:51):

From: Florian Haftmann <florian.haftmann@cit.tum.de>

Code generation: non-overloaded function specifications for a class
parameter are now permitted and effectively turn this class parameter
into an ordinary function in generated code; this allows to dissociate a
class parameter from its origin class in generated code.

It is still possible to specify code equations for instances of that
class parameter.

See 1bc9496f0ce6.

This change is a nice example how things emerge non-invasively after
carefully re-pondering ancient heritage in a well-tended code base.

For a practical application, see the follow-up changeset 35e22d4754d6.

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc


Last updated: Jan 14 2026 at 04:49 UTC