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.

`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.

Oh well. Thanks.

Last updated: Sep 25 2021 at 08:21 UTC