diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-01-26 15:07:04 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-01-26 15:07:04 +0100 |
| commit | 8b45125422a2b737ff660c798e00de073983f2cc (patch) | |
| tree | 97f764b29adeadd17ff8eb380a3f9eeab5c08818 /Bidir.agda | |
| parent | 53e656496f0dfc6b5d6b8b6e5caf5efc0e7ee404 (diff) | |
| download | bidiragda-8b45125422a2b737ff660c798e00de073983f2cc.tar.gz | |
open \==-Reasoning at top level
Diffstat (limited to 'Bidir.agda')
| -rw-r--r-- | Bidir.agda | 5 |
1 files changed, 1 insertions, 4 deletions
@@ -13,6 +13,7 @@ open import Relation.Nullary open import Relation.Nullary.Negation open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality +open Relation.Binary.PropositionalEquality.≡-Reasoning _>>=_ : {A B : Set} → Maybe A → (A → Maybe B) → Maybe B _>>=_ = flip (flip maybe′ nothing) @@ -101,7 +102,6 @@ lemma-lookupM-generate {A} i f [] a p with begin lookupM i empty ≡⟨ sym (lemma-lookupM-empty i) ⟩ nothing ∎ - where open Relation.Binary.PropositionalEquality.≡-Reasoning lemma-lookupM-generate i f [] a p | () lemma-lookupM-generate i f (i' ∷ is) a p with i ≟F i' lemma-lookupM-generate i f (.i ∷ is) a p | yes refl = lemma-from-just (begin @@ -112,7 +112,6 @@ lemma-lookupM-generate i f (.i ∷ is) a p | yes refl = lemma-from-just (begin lookupM i (insert i (f i) (generate f is)) ≡⟨ sym (lemma-lookupM-insert i (f i) (generate f is)) ⟩ just (f i) ∎) - where open Relation.Binary.PropositionalEquality.≡-Reasoning lemma-lookupM-generate i f (i' ∷ is) a p | no ¬p2 = lemma-lookupM-generate i f is a (begin just a ≡⟨ p ⟩ @@ -121,7 +120,6 @@ lemma-lookupM-generate i f (i' ∷ is) a p | no ¬p2 = lemma-lookupM-generate i lookupM i (insert i' (f i') (generate f is)) ≡⟨ sym (lemma-lookupM-insert-other i i' (f i') (generate f is) ¬p2) ⟩ lookupM i (generate f is) ∎) - where open Relation.Binary.PropositionalEquality.≡-Reasoning lemma-checkInsert-generate : {τ : Set} {n : ℕ} → (eq : EqInst τ) → (f : Fin n → τ) → (i : Fin n) → (is : List (Fin n)) → checkInsert eq i (f i) (generate f is) ≡ just (generate f (i ∷ is)) lemma-checkInsert-generate eq f i is with lookupM i (generate f is) | inspect (lookupM i) (generate f is) @@ -143,7 +141,6 @@ lemma-1 eq f (i ∷ is′) = begin (checkInsert eq i (f i) (generate f is′)) ≡⟨ lemma-checkInsert-generate eq f i is′ ⟩ just (generate f (i ∷ is′)) ∎ - where open Relation.Binary.PropositionalEquality.≡-Reasoning lemma-2 : {τ : Set} {n : ℕ} → (eq : EqInst τ) → (is : List (Fin n)) → (v : List τ) → (h : FinMapMaybe n τ) → just h ≡ assoc eq is v → map (flip lookup h) is ≡ map just v lemma-2 eq [] [] h p = refl |