From db1e29ec11c0cc0a874ef9df25b30abca960595d Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Mon, 3 Feb 2014 16:36:11 +0100 Subject: 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 --- FinMap.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'FinMap.agda') 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))) -- cgit v1.2.3