Stream: Beginner Questions

Topic: Additional type variable in an extended locale

view this post on Zulip Gergely Buday (Aug 11 2020 at 09:46):

For this extended locale:

locale preorder

begin

typedecl conf
type_synonym vm = "conf ⇒ conf ⇒ bool"

end

locale calculation = preorder +

assumes refl: "vm x x"

I get

locale calculation
assumes "calculation TYPE('a)"
Additional type variable(s) in locale specification "calculation": 'a

Why I get this error message?

And, do I understand correctly that calculation is a functor on the structure preorder here? I am using Standard ML terminology in this question.

view this post on Zulip Lukas Stevens (Aug 11 2020 at 13:16):

vm is a type_synonym but you are also using it as a term. That does not make sense. Note that Isabelle/HOL is simply typed so types cannot appear in terms.

view this post on Zulip Gergely Buday (Aug 12 2020 at 07:19):

Oh well. Thanks.

Last updated: Dec 21 2024 at 16:20 UTC