From 27621992ade2aa69119f7cdd9ea1c8ee3499c338 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 28 Nov 2025 16:25:46 -0800 Subject: [PATCH] Rename a helper Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index a637609..d3d97f3 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -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¹