Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Accessing definitions in a locale from outside

Email Gateway (May 15 2026 at 07:56):

From: Tobias Nipkow <nipkow@in.tum.de>

Hi,

If I define some function in a locale, how do I access the defining equations
outside the local from ML? Top-level function definitions can be accessed via
Spec_Rules.retrieve, but for functions from a locale, it returns an empty list,
although the constant itself is known, meaning @{const L.f} works fine (with the
locale parameters as additional arguments).

Thanks
Tobias

smime.p7s

Email Gateway (May 18 2026 at 07:16):

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

Hi Tobias,

If I define some function in a locale, how do I access the defining
equations outside the local from ML? Top-level function definitions can
be accessed via Spec_Rules.retrieve, but for functions from a locale, it
returns an empty list, although the constant itself is known, meaning
@{const L.f} works fine (with the locale parameters as additional
arguments).

not 100% sure what your actual application is, but the following schema
is a starting point:

locale nat
begin

datatype T = Zero | Succ T

primrec sym_dec :: ‹T ⇒ T›
where
‹sym_dec Zero = Succ Zero›
| ‹sym_dec (Succ n) = n›

ML_val ‹
Spec_Rules.retrieve \<^context> \<^term>‹sym_dec›
›

end

It is important that you retrieve the spec rules relative to the locale
context (Locale.init).

Hope this helps,
Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

Last updated: May 23 2026 at 03:31 UTC