diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-12-10 11:48:15 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-12-10 11:48:15 +0100 |
| commit | 1625dfe1e5ee62ffef1884a38ba4599b9c5510e4 (patch) | |
| tree | 9a39a8725548f03e7d6cb2b9626b5fd7432b9318 | |
| parent | b623a3e175a96b9732446a312080fa564ae80f71 (diff) | |
| download | bidiragda-1625dfe1e5ee62ffef1884a38ba4599b9c5510e4.tar.gz | |
get rid of contraposition
Using function composition in all other places already.
| -rw-r--r-- | FinMap.agda | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/FinMap.agda b/FinMap.agda index bdead33..861076a 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -10,7 +10,7 @@ open import Data.List using (List ; [] ; _∷_ ; map ; zip) open import Data.Product using (_×_ ; _,_) open import Function using (id ; _∘_ ; flip) open import Relation.Nullary using (yes ; no) -open import Relation.Nullary.Negation using (contradiction ; contraposition) +open import Relation.Nullary.Negation using (contradiction) open import Relation.Binary.Core using (_≡_ ; refl ; _≢_) open import Relation.Binary.PropositionalEquality using (cong ; sym ; _≗_ ; trans) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) @@ -66,7 +66,7 @@ lemma-lookupM-insert-other : {A : Set} {n : â„•} → (i j : Fin n) → (a : A) â lemma-lookupM-insert-other zero zero a m p = contradiction refl p lemma-lookupM-insert-other zero (suc j) a (x ∷ xs) p = refl lemma-lookupM-insert-other (suc i) zero a (x ∷ xs) p = refl -lemma-lookupM-insert-other (suc i) (suc j) a (x ∷ xs) p = lemma-lookupM-insert-other i j a xs (contraposition (cong suc) p) +lemma-lookupM-insert-other (suc i) (suc j) a (x ∷ xs) p = lemma-lookupM-insert-other i j a xs (p ∘ cong suc) just-injective : {A : Set} → {x y : A} → _≡_ {_} {Maybe A} (just x) (just y) → x ≡ y just-injective refl = refl |