DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Slightly clean up import for in-dec for Graph edges

Browse Source
This commit is contained in:
Danila Fedorin 2024-11-16 15:15:42 -08:00
parent 4fba1fe79a
commit 9131214880
1 changed files with 5 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
Language/Graphs.agda
View File

@ -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))