小编vku*_*cak的帖子

我试图证明列表中的大小(元素数量)是非负的,但莱昂未能证明它 - 它只是超时.莱昂真的没有能力证明这个属性,还是我错误地使用它？我的出发点是我在文章"莱昂验证系统概述"中读到的一个功能.

import leon.lang._
import leon.annotation._

object ListSize {
  sealed abstract class List
  case class Cons(head: Int, tail: List) extends List
  case object Nil extends List

  def size(l: List) : Int = (l match {
    case Nil => 0
    case Cons(_, t) => 1 + size(t)
  }) ensuring(_ >= 0)
}