From ccb7abc501e68b7692f9a621c3ce933ce12c152a Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 30 Apr 2024 19:15:38 -0700 Subject: [PATCH] Remove unused code from Utils Signed-off-by: Danila Fedorin --- Language/Graphs.agda | 2 +- Utils.agda | 10 ---------- 2 files changed, 1 insertion(+), 11 deletions(-) diff --git a/Language/Graphs.agda b/Language/Graphs.agda index cac85cc..d4f8bfd 100644 --- a/Language/Graphs.agda +++ b/Language/Graphs.agda @@ -15,7 +15,7 @@ open import Data.Vec.Properties using (cast-is-id; ++-assoc; lookup-++ˡ; cast-s open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst; trans) open import Lattice -open import Utils using (x∈xs⇒fx∈fxs; _⊗_; _,_; ∈-cartesianProduct) +open import Utils using (x∈xs⇒fx∈fxs; ∈-cartesianProduct) record Graph : Set where constructor MkGraph diff --git a/Utils.agda b/Utils.agda index 60edd25..6223787 100644 --- a/Utils.agda +++ b/Utils.agda @@ -71,16 +71,6 @@ data Pairwise {a} {b} {c} {A : Set a} {B : Set b} (P : A → B → Set c) : List P x y → Pairwise P xs ys → Pairwise P (x ∷ xs) (y ∷ ys) -infixr 2 _⊗_ -data _⊗_ {a p q} {A : Set a} (P : A → Set p) (Q : A → Set q) : A → Set (a ⊔ℓ p ⊔ℓ q) where - _,_ : ∀ {val : A} → P val → Q val → (P ⊗ Q) val - -proj₁ : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} {a : A} → (P ⊗ Q) a → P a -proj₁ (v , _) = v - -proj₂ : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} {a : A} → (P ⊗ Q) a → Q a -proj₂ (_ , v) = v - ∈-cartesianProduct : ∀ {a b} {A : Set a} {B : Set b} {x : A} {xs : List A} {y : B} {ys : List B} → x ∈ xs → y ∈ ys → (x Prod., y) ∈ cartesianProduct xs ys