Stream: Beginner Questions

Topic: locale syntax

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?

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"

Lukas Stevens (Aug 25 2020 at 12:35):

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

Lukas Stevens (Aug 25 2020 at 12:35):

fixes has to come before begin

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"

Mathias Fleury (Aug 25 2020 at 12:38):

Yeah splitting locales is very standard (even if annoying)

Last updated: Dec 21 2024 at 16:20 UTC