Email Gateway (Aug 22 2022 at 12:18): Email Gateway (Aug 22 2022 at 12:18):From: Peter Gammie <peteg42@gmail.com>
Hi,
Is this supposed to work? I’m guessing not. The error that arises is not very good (for recent repository versions and 2016-RC2).
In my actual use-case I assume “Q b” where Q implies P, and the definition is non-trivial. As a syntactic nicety I don’t want to have to provide “a” when I instantiate locale m. I can make this work for now by saying: assumes “a = b” but it is ugly.
cheers,
peter
theory l
imports Main
begin
locale l =
fixes a
assumes "P a"
locale m = l +
fixes b
(* assumes “P b” *)
defines "a == b"
end
Email Gateway (Aug 22 2022 at 12:18):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Peter,
"defines" used to work like this until around 2008. Since then, it does not really make
sense to use "defines" in a locale because you still have to provide the defined parameter
in the instantiations. Normally, sublocales work much better.
consts P :: "'a ⇒ bool"
consts Q :: "'a ⇒ bool"
consts f :: "'a ⇒ 'a"
locale l =
fixes a
assumes "P a"
locale m =
fixes b
assumes "Q b"
begin
sublocale l "f b" apply(unfold_locales) sorry
end
Hope this helps,
Andreas
Email Gateway (Aug 22 2022 at 12:19):From: Peter Gammie <peteg42@gmail.com>
Thanks Andreas. I ended up doing this.
cheers,
peter
Last updated: Nov 21 2024 at 12:39 UTC