You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
In the Induction section of Proving Theorems, the below example does not make a reference to leon.proof:
importleon.collection._// for Listimportleon.lang._// for holdsobjectExample {
defreverseReverse[T](l: List[T]):Boolean= {
l.reverse.reverse == l
}.holds
}
Which is then needed in the following steps (for because, check and trivial calls):
defreverseReverse[T](l: List[T]):Boolean= {
l.reverse.reverse == l because {
l match {
caseNil() => check { Nil[T]().reverse.reverse ==Nil[T]() }
caseCons(x, xs) => check { (x :: xs).reverse.reverse == (x :: xs) }
}
}
}.holds
defreverseReverse[T](l: List[T]):Boolean= {
l.reverse.reverse == l because {
l match {
caseNil() => trivial
caseCons(x, xs) => check { (xs.reverse :+ x).reverse == (x :: xs) }
}
}
}.holds
The text was updated successfully, but these errors were encountered:
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.
In the Induction section of Proving Theorems, the below example does not make a reference to
leon.proof
:Which is then needed in the following steps (for
because
,check
andtrivial
calls):The text was updated successfully, but these errors were encountered: