Remove unused code from Utils
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
91b5d108f6
commit
ccb7abc501
|
@ -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 Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst; trans)
|
||||||
|
|
||||||
open import Lattice
|
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
|
record Graph : Set where
|
||||||
constructor MkGraph
|
constructor MkGraph
|
||||||
|
|
10
Utils.agda
10
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 →
|
P x y → Pairwise P xs ys →
|
||||||
Pairwise P (x ∷ xs) (y ∷ 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}
|
∈-cartesianProduct : ∀ {a b} {A : Set a} {B : Set b}
|
||||||
{x : A} {xs : List A} {y : B} {ys : List B} →
|
{x : A} {xs : List A} {y : B} {ys : List B} →
|
||||||
x ∈ xs → y ∈ ys → (x Prod., y) ∈ cartesianProduct xs ys
|
x ∈ xs → y ∈ ys → (x Prod., y) ∈ cartesianProduct xs ys
|
||||||
|
|
Loading…
Reference in New Issue
Block a user