From aa327061205d0e309ed9bee13efd34ec83167b42 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 23 Dec 2025 14:07:45 -0800 Subject: [PATCH] Fix typo Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index fc4b450..3e0dd3c 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -252,10 +252,10 @@ record Graph : Set where ... | yes refl | yes refl = f (adj n₁ n₂) ... | _ | _ = adj n₁' n₂' - Adjecency-append : ∀ {n₁ n₂ : Node} → List (Path n₁ n₂) → Adjacency → Adjacency - Adjecency-append {n₁} {n₂} ps = Adjacency-update n₁ n₂ (ps ++ˡ_) + Adjacency-append : ∀ {n₁ n₂ : Node} → List (Path n₁ n₂) → Adjacency → Adjacency + Adjacency-append {n₁} {n₂} ps = Adjacency-update n₁ n₂ (ps ++ˡ_) - Adjacency-append-monotonic : ∀ {adj n₁ n₂ n₁' n₂'} {ps : List (Path n₁ n₂)} {p : Path n₁' n₂'} → p ∈ˡ adj n₁' n₂' → p ∈ˡ Adjecency-append ps adj n₁' n₂' + Adjacency-append-monotonic : ∀ {adj n₁ n₂ n₁' n₂'} {ps : List (Path n₁ n₂)} {p : Path n₁' n₂'} → p ∈ˡ adj n₁' n₂' → p ∈ˡ Adjacency-append ps adj n₁' n₂' Adjacency-append-monotonic {adj} {n₁} {n₂} {n₁'} {n₂'} {ps} p∈adj with n₁ ≟ n₁' | n₂ ≟ n₂' ... | yes refl | yes refl = ∈ˡ-++⁺ʳ ps p∈adj