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

Delete debugging code

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-07-25 17:18:31 +02:00
parent 2808759338
commit 7e099a2561
1 changed files with 0 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Lattice/Builder.agda
View File

@ -723,9 +723,6 @@ pathJoin'-related' {Ls = Ls} p₁ p₂ p₃ p₂⊔p₃ p₂⊔?p₃=justp₂⊔
| eqPath'-pathJoin'-cong {Ls = Ls} (eqPath'-refl Ls p₁) p₂⊔p₃≈p₃⊔p₂ | eqPath'-pathJoin'-cong {Ls = Ls} (eqPath'-refl Ls p₁) p₂⊔p₃≈p₃⊔p₂
... | nothing | nothing | nothing | ≈-nothing | refl | ≈-nothing = refl ... | nothing | nothing | nothing | ≈-nothing | refl | ≈-nothing = refl
-- fact: pathJoin' Ls p₃ p₂ ≡ just p₃⊔p₂
pathJoin'-assoc : ∀ {a} {Ls : Layers a} → PartialAssoc (eqPath' Ls) (pathJoin' Ls) pathJoin'-assoc : ∀ {a} {Ls : Layers a} → PartialAssoc (eqPath' Ls) (pathJoin' Ls)
pathJoin'-assoc {Ls = single l} lv₁ lv₂ lv₃ = lvJoin-assoc (toList l) lv₁ lv₂ lv₃ pathJoin'-assoc {Ls = single l} lv₁ lv₂ lv₃ = lvJoin-assoc (toList l) lv₁ lv₂ lv₃
pathJoin'-assoc {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃) pathJoin'-assoc {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃)