Gergely Buday (Aug 10 2020 at 12:33): Gergely Buday (Aug 10 2020 at 12:33):I am trying to use type declarations in a locale:
locale preorder =
typedecl conf
type_synonym vm = "conf ⇒ conf ⇒ bool"
for the first line I get
Outer syntax error⌂: context element expected,
but end-of-input⌂ was found
What's wrong with this definition?
Lukas Stevens (Aug 10 2020 at 12:59):For the syntax of locale declarations see Chapter 5 of https://isabelle.in.tum.de/doc/isar-ref.pdf.
Lukas Stevens (Aug 10 2020 at 13:00):The railroad diagram shows you how a syntactically correct locale declaration must look like.
Manuel Eberl (Aug 10 2020 at 13:03):(deleted wrong claim)
Manuel Eberl (Aug 10 2020 at 13:06):You probably want to write
locale preorder
begin
typedecl conf
type_synonym vm = "conf ⇒ conf ⇒ bool"
I was not aware you could even do typedecl and type_synonym inside a locale, but apparently you can. Today I learnt.
You only need the = if you want to base your local on another locale, or add fixes/assumes.
Last updated: Apr 23 2024 at 16:19 UTC