scala - 通用抽象类型的问题

Question

我有一个抽象的 Stack 类型如下

abstract class Stack[T] {
  def empty  : Stack[T]
  def pop () : (Option[T], Stack[T])
  def push (e : T) : Stack[T]
  def size : BigInt
}

我想验证 pop 是否返回最后推送的元素:

// ok
def test_v1[T] (e : T, s : Stack[T]) : Boolean = {
  s.push(e).pop()._1 match {
    case Some(e2) => e == e2
    case _        => false
  }
} holds

// failed
def test_v2[T] (e : T, s : Stack[T]) : Boolean = {
  s.push(e).pop()._1 == Some(e)
} holds

这两个引理是等价的，但 Leon 无法识别第二个引理中的类型参数。有趣的是，莱昂在Stack 是具体的或非通用的(有关示例，请参见下面的链接)。这是 Leon 的特性还是只是一个错误？

可以找到完整的示例代码here .

Answer 1

我在你的要点链接中尝试了这个例子(在“可以在这里下找到”)并且它在当前版本的 Leon 中工作，在线和 git 存储库中。因此，如果这是一个错误，现在已修复。如果您有任何相关问题，我们很乐意回答，因为 Leon 目前仅支持对象和案例类，因此与完整的 Scala 相比存在差异。