Stream: Beginner Questions

Topic: type declarations in a locale


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Lukas Stevens (Aug 10 2020 at 13:00):

The railroad diagram shows you how a syntactically correct locale declaration must look like.

view this post on Zulip Manuel Eberl (Aug 10 2020 at 13:03):

(deleted wrong claim)

view this post on Zulip 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: Aug 15 2022 at 02:13 UTC