leon
leon copied to clipboard
Missing import statement in documentation example
In the Induction section of Proving Theorems, the below example does not make a reference to leon.proof
:
import leon.collection._ // for List
import leon.lang._ // for holds
object Example {
def reverseReverse[T](l: List[T]): Boolean = {
l.reverse.reverse == l
}.holds
}
Which is then needed in the following steps (for because
, check
and trivial
calls):
def reverseReverse[T](l: List[T]): Boolean = {
l.reverse.reverse == l because {
l match {
case Nil() => check { Nil[T]().reverse.reverse == Nil[T]() }
case Cons(x, xs) => check { (x :: xs).reverse.reverse == (x :: xs) }
}
}
}.holds
def reverseReverse[T](l: List[T]): Boolean = {
l.reverse.reverse == l because {
l match {
case Nil() => trivial
case Cons(x, xs) => check { (xs.reverse :+ x).reverse == (x :: xs) }
}
}
}.holds
@mantognini Maybe you want to look into this?
While because
and check
were already introduced before, we could add import leon.proof._ // for check, trivial and because
as well to make things more obvious and simplify copy-pasting the examples. It would also be a bit more consistent with other snippets.