Stream: General

Topic: Attributes and locale interpretations

Lukas Stevens (Sep 21 2023 at 13:40):

I wrote some ML code that declares a locale and defines two datatypes and a constant inside this locale. The code marks some theorems of the data types (e.g. selectors) and the definition as code_unfold. I'd like to interpret this locale in an anonymous context where the corresponding theorems should be marked as code_unfold. Unfortunately, this only seems to work with global_interpretation. Is it possible to avoid global_interpretation?

Example below:

theory Scratch imports Main
begin

locale foo
begin
definition "bar = True"
declare bar_def[code_unfold]
end

context
begin
interpretation foo .
definition "foobar1 = bar"
(* Does not work *)
export_code foobar1 in SML
end

context
begin
global_interpretation foo .
definition "foobar2 = bar"
(* Does work *)
export_code foobar2 in SML
end

end

Last updated: Dec 30 2024 at 16:22 UTC