Stream: Beginner Questions

Topic: locale syntax


view this post on Zulip Gergely Buday (Aug 25 2020 at 12:31):

I tried the following:

locale preorder

begin

typedecl conf
fixes vm :: "conf ⇒ conf ⇒ bool"

end

Isabelle/jEdit does not like "fixes" as it is not a command. I took a look at the Isar Reference Manual, 5.7.2 Locale declarations, but the syntax diagram is not detailed enough to figure out why the system complains about "fixes" here.

What's wrong with this?

view this post on Zulip Mathias Fleury (Aug 25 2020 at 12:35):

The easiest is to look at other examples that work:

$ grep --include \*.thy -A 3 -r locale *
src/ZF/Induct/FoldSet.thy:locale fold_typing =
src/ZF/Induct/FoldSet.thy- fixes A and B and e and f
src/ZF/Induct/FoldSet.thy- assumes ftype [intro,simp]:  "[|x \<in> A; y \<in> B|] ==> f(x,y) \<in> B"
src/ZF/Induct/FoldSet.thy-     and etype [intro,simp]:  "e \<in> B"

view this post on Zulip Lukas Stevens (Aug 25 2020 at 12:35):

locale preorder =
fixes vm :: ...
begin
end

view this post on Zulip Lukas Stevens (Aug 25 2020 at 12:35):

fixes has to come before begin

view this post on Zulip Gergely Buday (Aug 25 2020 at 12:37):

I came up with

locale conf
begin
typedecl conf
end

locale preorder = conf +

fixes vm :: "conf ⇒ conf ⇒ bool"

view this post on Zulip Mathias Fleury (Aug 25 2020 at 12:38):

Yeah splitting locales is very standard (even if annoying)


Last updated: Sep 25 2022 at 23:25 UTC