# ReverseReverse3 FIXED

## Description

using a definition from haskell2010-1.1.1.0

## Definitions (download)

module Definitions where open import Data.List rev : ∀ {a} {A : Set a} → List A → List A → List A rev [] a = a rev (x ∷ xs) a = rev xs (x ∷ a) myreverse : ∀ {a} {A : Set a} → List A → List A myreverse {a}{A} xs = rev xs []

## 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 | Rotsor | 195 | 2015-02-01 06:52:20 JST |

2 | trigott | 470 | 2014-11-15 07:48:13 JST |

3 | Lost_dog_ | 764 | 2014-04-20 10:54:21 JST |