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

Rename a helper

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-11-28 16:25:46 -08:00
parent e409cceae5
commit 27621992ad
1 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
Lattice/Builder.agda
View File

@ -72,25 +72,25 @@ record Graph : Set where
seedWithEdges : ∀ (es : List Edge) → (∀ {e} → e ∈ˡ es → e ∈ˡ edges) → Adjacency
seedWithEdges es e∈es⇒e∈edges = foldr (λ ((n₁ , n₂) , n₁n₂∈edges) → Adjacency-update n₁ n₂ ((last n₁n₂∈edges) ∷_)) (λ n₁ n₂ → []) (mapWith∈ˡ es (λ {e} e∈es → (e , e∈es⇒e∈edges e∈es)))
edge∈seedWithEdges : ∀ {n₁ n₂ es} → (e∈es⇒e∈edges : ∀ {e} → e ∈ˡ es → e ∈ˡ edges) → ∀ (n₁n₂∈es : (n₁ , n₂) ∈ˡ es) → (last (e∈es⇒e∈edges n₁n₂∈es)) ∈ˡ seedWithEdges es e∈es⇒e∈edges n₁ n₂
edge∈seedWithEdges {es = []} e∈es⇒e∈edges ()
edge∈seedWithEdges {es = (n₁' , n₂') ∷ es} e∈es⇒e∈edges (here refl)
e∈seedWithEdges : ∀ {n₁ n₂ es} → (e∈es⇒e∈edges : ∀ {e} → e ∈ˡ es → e ∈ˡ edges) → ∀ (n₁n₂∈es : (n₁ , n₂) ∈ˡ es) → (last (e∈es⇒e∈edges n₁n₂∈es)) ∈ˡ seedWithEdges es e∈es⇒e∈edges n₁ n₂
e∈seedWithEdges {es = []} e∈es⇒e∈edges ()
e∈seedWithEdges {es = (n₁' , n₂') ∷ es} e∈es⇒e∈edges (here refl)
with n₁' ≟ n₁' | n₂' ≟ n₂'
... | yes refl | yes refl = here refl
... | no n₁'≢n₁' | _ = ⊥-elim (n₁'≢n₁' refl)
... | _ | no n₂'≢n₂' = ⊥-elim (n₂'≢n₂' refl)
edge∈seedWithEdges {n₁} {n₂} {es = (n₁' , n₂') ∷ es} e∈es⇒e∈edges (there n₁n₂∈es)
e∈seedWithEdges {n₁} {n₂} {es = (n₁' , n₂') ∷ es} e∈es⇒e∈edges (there n₁n₂∈es)
with n₁' ≟ n₁ | n₂' ≟ n₂
... | yes refl | yes refl = there (edge∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es)
... | no _ | no _ = edge∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es
... | no _ | yes _ = edge∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es
... | yes refl | no _ = edge∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es
... | yes refl | yes refl = there (e∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es)
... | no _ | no _ = e∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es
... | no _ | yes _ = e∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es
... | yes refl | no _ = e∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es
adj¹ : Adjacency
adj¹ = seedWithEdges edges (λ x → x)
edge∈adj¹ : ∀ {n₁ n₂} (n₁n₂∈edges : (n₁ , n₂) ∈ˡ edges) → (last n₁n₂∈edges) ∈ˡ adj¹ n₁ n₂
edge∈adj¹ = edge∈seedWithEdges (λ x → x)
edge∈adj¹ = e∈seedWithEdges (λ x → x)
throughAll : List Node → Adjacency
throughAll = foldr through adj¹