Email Gateway (Aug 22 2022 at 11:33): Email Gateway (Aug 22 2022 at 11:33):From: Peter Lammich <lammich@in.tum.de>
Hi,
I ran into the following unexpected behaviour with locales:
theory Scratch
imports Main
begin
locale A begin
definition "name ≡ True"
end
interpretation foo!: A by (unfold_locales) (* If this line is
removed, everything works as expected. *)
locale B = A +
assumes "name" (* Name is a FREE VARIABLE here*)
end
When defining locale B, I would have expected "name" to reference to the
definition in A. However, if there is an interpretation of A before,
"name" is a free variable in the definition of B, and I have no idea how
to access "name" from A?
Questions:
1. Is this the correct behaviour?
2. How to correctly reference "name" from A, in the definition of B?
Email Gateway (Aug 22 2022 at 11:34):From: Peter Lammich <lammich@in.tum.de>
This was a boiled down example. The original example had a parameter, and i
used the interpretation to get code theorems for the constants defined in this
locale.
Enviado atraves de Huawei Mobile
\-------- Originalnachricht --------
Last updated: Nov 21 2024 at 12:39 UTC