diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-03 16:36:11 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2014-02-03 16:36:11 +0100 |
| commit | db1e29ec11c0cc0a874ef9df25b30abca960595d (patch) | |
| tree | 3abef25f15ac6067a34eeda7ff8ee823f90a6cbb /FinMap.agda | |
| parent | 39bae2aebe94d04b981e006e33fcf96c86acbf56 (diff) | |
| download | bidiragda-db1e29ec11c0cc0a874ef9df25b30abca960595d.tar.gz | |
make things compile with 2.3.0.1
* Remove let patter , match = foo usage
* Remove Qualified.infix-symbol usage
* Add non-obvious absurd patterns
* Qualify constructors
Diffstat (limited to 'FinMap.agda')
| -rw-r--r-- | FinMap.agda | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/FinMap.agda b/FinMap.agda index ea4f49b..052ed6f 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -94,7 +94,7 @@ lemma-tabulate-∘ : {n : ℕ} {A : Set} → {f g : Fin n → A} → f ≗ g → lemma-tabulate-∘ {zero} {_} {f} {g} f≗g = refl lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = cong₂ _∷_ (f≗g zero) (lemma-tabulate-∘ (f≗g ∘ suc)) -lemma-fromFunc-tabulate : {n : ℕ} {A : Set} → (f : Fin n → A) → fromFunc f ≡ tabulate (just ∘ f) +lemma-fromFunc-tabulate : {n : ℕ} {A : Set} → (f : Fin n → A) → fromFunc f ≡ tabulate (Maybe.just ∘ f) lemma-fromFunc-tabulate {zero} f = refl lemma-fromFunc-tabulate {suc _} f = cong (_∷_ (just (f zero))) (lemma-fromFunc-tabulate (f ∘ suc)) @@ -113,8 +113,8 @@ lemma-disjoint-union {n} {m} f t = trans (lemma-tabulate-∘ (lemma-inner t)) (s ≡⟨ cong (maybe′ just (lookupM x (fromFunc f))) (lemma-lookupM-empty x) ⟩ lookupM x (fromFunc f) ≡⟨ cong (lookupM x) (lemma-fromFunc-tabulate f) ⟩ - lookupM x (tabulate (just ∘ f)) - ≡⟨ lookup∘tabulate (just ∘ f) x ⟩ + lookupM x (tabulate (Maybe.just ∘ f)) + ≡⟨ lookup∘tabulate (Maybe.just ∘ f) x ⟩ just (f x) ∎ lemma-inner (t ∷ ts) x with x ≟ t lemma-inner (.x ∷ ts) x | yes refl = cong (maybe′ just (lookupM x (delete-many (x ∷ ts) (fromFunc f)))) (lemma-lookupM-insert x (f x) (restrict f (toList ts))) |