Dafny中的多态性

Question

我正试着在Dafny中做多态性，但我不能让它工作。我找不到任何文档来帮助我解决这个问题。下面是代码：https://rise4fun.com/Dafny/uQ1w

trait Atom {
  var Leaf? : bool;
}

class Leaf extends Atom {
  constructor() {
    this.Leaf? := true;
  }
}

class Node extends Atom {
  var left : Atom;

  constructor() {
    this.Leaf? := false;
    this.left := new Leaf();
  }
}

method Main() {
  var root := new Node();
  root.left := new Node();

  root.left.left := new Node();
}

错误：

Dafny 2.1.1.10209
stdin.dfy(24,12): Error: member left does not exist in trait Atom
1 resolution/type errors detected in stdin.dfy