From 7e1f70210bb130f40ac7363414d25d7292d0e63d Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 30 Jul 2023 22:26:05 -0700 Subject: [PATCH] Remove trailing space --- Map.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Map.agda b/Map.agda index c0bd28e..f8ae3f7 100644 --- a/Map.agda +++ b/Map.agda @@ -411,7 +411,7 @@ module _ (_≈_ : B → B → Set b) where rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₁v₂v₃∈m₁₂m₃ = (f v₁ (f v₂ v₃) , (f-assoc v₁ v₂ v₃ , I.union-combines u₁ (I.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I.union-combines u₂ u₃ v₂∈e₂ v₃∈e₃))) - union-assoc₂ : subset (union f m₁ (union f m₂ m₃)) (union f (union f m₁ m₂) m₃) + union-assoc₂ : subset (union f m₁ (union f m₂ m₃)) (union f (union f m₁ m₂) m₃) union-assoc₂ k v k,v∈m₁m₂₃ with Expr-Provenance f k ((` m₁) ∪ ((` m₂) ∪ (` m₃))) (∈-cong proj₁ k,v∈m₁m₂₃) ... | (_ , (in₂ k∉ke₁ (in₂ k∉ke₂ (single {v₃} v₃∈e₃)) , v₃∈m₁m₂₃))