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

Fix typo

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2025-12-23 14:07:45 -08:00
parent 4b0541caf5
commit aa32706120
1 changed files with 3 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
Lattice/Builder.agda
View File

@@ -252,10 +252,10 @@ record Graph : Set where
... | yes refl | yes refl = f (adj n₁ n₂) ... | yes refl | yes refl = f (adj n₁ n₂)
... | _ | _ = adj n₁' n₂' ... | _ | _ = adj n₁' n₂'
Adjecency-append : ∀ {n₁ n₂ : Node} → List (Path n₁ n₂) → Adjacency → Adjacency Adjacency-append : ∀ {n₁ n₂ : Node} → List (Path n₁ n₂) → Adjacency → Adjacency
Adjecency-append {n₁} {n₂} ps = Adjacency-update n₁ n₂ (ps ++ˡ_) 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 Adjacency-append-monotonic {adj} {n₁} {n₂} {n₁'} {n₂'} {ps} p∈adj
with n₁ ≟ n₁' | n₂ ≟ n₂' with n₁ ≟ n₁' | n₂ ≟ n₂'
... | yes refl | yes refl = ∈ˡ-++⁺ʳ ps p∈adj ... | yes refl | yes refl = ∈ˡ-++⁺ʳ ps p∈adj