区域设置忽略操作符号

Question

下列各项运作良好：

class test1 = semilattice_sup +
  fixes x :: "'a"
  assumes "x < y"

但是当我用class代替locale时

locale test2 = semilattice_sup +
  fixes x :: "'a"
  assumes "x < y"

我知道错误：

Type unification failed: Variable 'a::type not of sort ord

错误可以按以下方式修正：

locale test2 = semilattice_sup +
  fixes x :: "'a"
  assumes "less x y"

但是可以使用<表示法吗？

更新

下面是一个类似的问题：

datatype 'a ty = A | B

instantiation ty :: (order) order
begin
definition "x < y ≡ x = A ∧ y = B"
definition "x ≤ y ≡ (x :: 'a ty) = y ∨ x < y"
instance
  apply intro_classes
  using less_eq_ty_def less_ty_def by auto
end

locale loc = semilattice_sup +
  fixes f :: "'a ⇒ 't :: order"
begin
definition "g ≡ inv f"
end

class cls = semilattice_sup +
  fixes f :: "'a ⇒ 'a ty"
begin
interpretation base: loc .
abbreviation "g ≡ base.g"
end

如果出现以下错误，解释将失败：

Type unification failed: Variable 'a::type not of sort semilattice_sup

Answer 1

将会

locale test2 =
  fixes x :: "'a :: semilattice_sup"
  assumes "x < y"

是你的选择吗？在这种情况下，您不再将您的区域设置建立在另一个区域设置之上，而是要求x类型作为类semilattice_sup的一个实例，这允许您为less使用漂亮的infix语法。