For this extended locale:
type_synonym vm = "conf ⇒ conf ⇒ bool"
locale calculation = preorder +
assumes refl: "vm x x"
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 2022 at 23:25 UTC