From 913121488069a20cdfd40777a8777eb3744c415e Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 16 Nov 2024 15:15:42 -0800 Subject: [PATCH] Slightly clean up import for in-dec for Graph edges --- Language/Graphs.agda | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Language/Graphs.agda b/Language/Graphs.agda index 01d8e0a..6dd07c3 100644 --- a/Language/Graphs.agda +++ b/Language/Graphs.agda @@ -12,7 +12,6 @@ open import Data.List.Relation.Unary.Any as RelAny using () open import Data.Nat as Nat using (ℕ; suc) open import Data.Nat.Properties using (+-assoc; +-comm) open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂) -open import Data.Product.Properties as ProdProp using () open import Data.Vec using (Vec; []; _∷_; lookup; cast; _++_) open import Data.Vec.Properties using (cast-is-id; ++-assoc; lookup-++ˡ; cast-sym; ++-identityʳ; lookup-++ʳ) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst; trans) @@ -148,7 +147,11 @@ private finValues-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (finValues-complete n' f')) module _ (g : Graph) where - open import Data.List.Membership.DecPropositional (ProdProp.≡-dec (FinProp._≟_ {Graph.size g}) (FinProp._≟_ {Graph.size g})) using (_∈?_) + open import Data.Product.Properties as ProdProp using () + private _≟_ = ProdProp.≡-dec (FinProp._≟_ {Graph.size g}) + (FinProp._≟_ {Graph.size g}) + + open import Data.List.Membership.DecPropositional (_≟_) using (_∈?_) indices : List (Graph.Index g) indices = proj₁ (finValues (Graph.size g))