ReverseReverse2

Description

using a definition from stdlib(0.6).

Definitions (download)

module Definitions where

open import Data.List

myreverse : ∀ {a} {A : Set a} → List A → List A
myreverse = foldl (λ rev x → x ∷ rev) []

Theorem (download)

module Theorem where

open import Definitions

open import Data.List
open import Relation.Binary.PropositionalEquality

postulate
  revrev : ∀ {a} {A : Set a} (xs : List A) → myreverse (myreverse xs) ≡ xs

Verifier

module Verifier where

open import Definitions
open import Theorem

open import Data.List
open import Relation.Binary.PropositionalEquality

verify : ∀ {a} {A : Set a} (xs : List A) → myreverse (myreverse xs) ≡ xs
verify = revrev

Proofs

Rank Prover Size Date
1 Lost_dog_ 411 2014-04-20 10:48:04 JST
2 trigott 543 2014-11-15 07:21:33 JST