Copyright | (c) Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
Documentation.SBV.Examples.TP.RevAcc
Description
Proves that the accummulating version of reverse is equivalent to the standard definition.
Reversing with an accummulator.
rev :: SymVal a => SList a -> SList a Source #
Given revAcc
, we can reverse a list by providing the empty list as the initial accumulator.
Correctness proof
correctness :: SymVal a => IO (Proof (Forall "xs" [a] -> SBool)) Source #
Correctness the function rev
. We have:
>>>
correctness @Integer
Inductive lemma: revAccCorrect Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Step: 3 Q.E.D. Step: 4 Q.E.D. Result: Q.E.D. Lemma: revCorrect Q.E.D. [Proven] revCorrect :: Ɐxs ∷ [Integer] → Bool