多态类

多态类可以用来系统地引入表示代数的符号系统。

例如，让我们从库类的草图开始 Eq 它引入了等价关系：

class Eq[t] {
  virtual fun == : t * t -> bool;
  virtual fun != (x:t,y:t):bool => not (x == y);

  axiom reflex(x:t): x == x;
  axiom sym(x:t, y:t): (x == y) == (y == x);
  axiom trans(x:t, y:t, z:t): x == y and y == z implies x == z;

  fun eq(x:t, y:t)=> x == y;
  fun ne(x:t, y:t)=> x != y;
}

类只有一个类型参数 t . 二 virtual 首先介绍功能， == 等效性，以及 != 因为不相等。

类型 == 函数已给定，但未定义。我们只有接口。

不等价性被定义为等价性的否定。

接下来，我们有三个公理来指定所需的语义。

第一条公理， reflexivity ，表示值等于自身。

第二条公理， symmetry ，表示a如果x等于y，那么y等于x。

第三条公理， transitivity 如果x等于y，y等于z，那么z也等于z。

在这种情况下，这三条定律是一个完整的规范，而且，这三条定律是独立的，因为一条定律不能从另一条定律中推导出来。这两个性质意味着我们的规则实际上是数学公理。

Felix不要求 axioms 实际上是公理。然而，可以从所述公理导出的简单规则可以通过 lemma . 它的思想是引理可以从公理中被很容易地证明，以至于一个自动的定理证明者可以做到这一点，而不需要任何进一步的帮助。

你也可以 theorem 这是一个可以从公理中证明的规则，但是如果证明需要一个人，或者一个有证明助手的人来证明它的正确性。

最后，在我们的类中，我们有两个用虚函数定义的命名函数。注意这些函数不是虚函数。