From f2e72b54ce840f6d8c60b001e6da6e3dca1260ca Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 23 Jul 2023 21:34:24 -0700 Subject: [PATCH] Define unique as a data type to match stdlib All and Any --- Map.agda | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/Map.agda b/Map.agda index 1c88133..723306b 100644 --- a/Map.agda +++ b/Map.agda @@ -22,11 +22,12 @@ open import Data.Empty using (⊥) Map : Set (a ⊔ b) Map = List (A × B) -record ⊤' : Set (a ⊔ b) where - -Unique : List (A × B) → Set (a ⊔ b) -Unique [] = ⊤' -Unique ((k , _) ∷ xs) = All (λ (k' , _) → ¬ k ≡ k') xs × Unique xs +data Unique : List (A × B) → Set (a ⊔ b) where + empty : Unique [] + push : forall {k : A} {v : B} {xs : List (A × B)} + → All (λ (k' , _) → ¬ k ≡ k') xs + → Unique xs + → Unique ((k , v) ∷ xs) _∈_ : (A × B) → Map → Set (a ⊔ b) _∈_ p m = Data.List.Membership.Propositional._∈_ p m @@ -55,7 +56,7 @@ merge f m₁ m₂ = foldr (insert f) m₂ m₁ Map-functional : ∀ (k : A) (v v' : B) (xs : List (A × B)) → Unique ((k , v) ∷ xs) → Data.List.Membership.Propositional._∈_ (k , v') ((k , v) ∷ xs) → v ≡ v' Map-functional k v v' _ _ (here k,v'≡k,v) = sym (cong proj₂ k,v'≡k,v) -Map-functional k v v' xs (k≢ , _) (there k,v'∈xs) = absurd (unique-not-in xs v' (k≢ , k,v'∈xs)) +Map-functional k v v' xs (push k≢ _) (there k,v'∈xs) = absurd (unique-not-in xs v' (k≢ , k,v'∈xs)) where absurd : ∀ {a} {A : Set a} → ⊥ → A absurd ()