Email Gateway (Aug 18 2022 at 17:44): Email Gateway (Aug 18 2022 at 17:44):From: Gudmund Grov <ggrov@staffmail.ed.ac.uk>
Dear all,
I am trying to store some data in the context of a locale which I can
later extract when working in that particular locale.
I thought I could use Proof_Data and local_setup as illustrated in the
following code snippet:
ML{*
structure Numbs = Proof_Data(type T = int fun init _ = 1);
val set_numbs = Numbs.map o K;
val get_numbs = Numbs.get;
*}
locale test
begin
local_setup{* set_numbs 2 *}
end
lemma (in test) "True"
ML_prf{* get_numbs @{context} *}
oops
However, get_numbs returns (the initial) 1 and not 2 as I would expect.
Does anyone know how I can achieve this?
Cheers,
Gudmund
Email Gateway (Aug 18 2022 at 17:45):From: Alexander Krauss <krauss@in.tum.de>
Hi Gudmund,
I thought I could use Proof_Data and local_setup as illustrated in the
following code snippet:
local_setup is rather non-standard. Grep tells me that it is currently
unused in the entire Isabelle distribution, and I don't actually know
what it is good for...
Instead, I think you should use a "declaration".
declaration {* fn _ => Context.map_proof (set_numbs 2) *}
Note that the extra argument _ is a morphism, since the declaration also
affects interpretations of the locale. If you have something more
interesting data than just numbers, you may want to apply the morphism
to it.
Hope this helps...
Alex
Email Gateway (Aug 18 2022 at 17:46):From: Gudmund Grov <ggrov@staffmail.ed.ac.uk>
Alex
Thanks - it was exactly what I needed.
Gudmund
Last updated: Apr 25 2024 at 16:19 UTC