diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-10-22 11:21:10 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-10-22 11:21:10 +0200 |
| commit | 9bc4007c94a94706acbfb02103581b3d94e38001 (patch) | |
| tree | 7c343f526502951e32fbf2fd8ac486ea8b42b569 /Precond.agda | |
| parent | 58038d636d9f1225f8355c22102823e3168ad56c (diff) | |
| download | bidiragda-9bc4007c94a94706acbfb02103581b3d94e38001.tar.gz | |
finally parameterize CheckInsert
Also adapt depending modules. Long lines generally become shorter. The
misleading name "EqInst" (hiding the decidability) got discarded.
Diffstat (limited to 'Precond.agda')
| -rw-r--r-- | Precond.agda | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/Precond.agda b/Precond.agda index 5011e41..a6d2d37 100644 --- a/Precond.agda +++ b/Precond.agda @@ -15,7 +15,8 @@ open import Relation.Binary.PropositionalEquality using (refl ; cong) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import FinMap using (FinMap ; FinMapMaybe ; union ; fromFunc ; empty ; insert) -open import CheckInsert using (EqInst ; checkInsert ; lemma-checkInsert-new) +import CheckInsert +open CheckInsert Carrier deq using (checkInsert ; lemma-checkInsert-new) open import BFF using (fmap ; _>>=_) import Bidir open Bidir Carrier deq using (lemma-∉-lookupM-assoc) @@ -67,8 +68,8 @@ different-assoc (u ∷ us) (v ∷ vs) p with different-assoc us vs (λ i j i≢j different-assoc (u ∷ us) (v ∷ vs) p | h , p' = insert u v h , (begin assoc (u ∷ us) (v ∷ vs) ≡⟨ refl ⟩ - assoc us vs >>= checkInsert deq u v - ≡⟨ cong (flip _>>=_ (checkInsert deq u v)) p' ⟩ - checkInsert deq u v h - ≡⟨ lemma-checkInsert-new deq u v h (lemma-∉-lookupM-assoc u us vs h p' (different-∉ u us p)) ⟩ + assoc us vs >>= checkInsert u v + ≡⟨ cong (flip _>>=_ (checkInsert u v)) p' ⟩ + checkInsert u v h + ≡⟨ lemma-checkInsert-new u v h (lemma-∉-lookupM-assoc u us vs h p' (different-∉ u us p)) ⟩ just (insert u v h) ∎) |