From 7e099a25615791fcb431c7af72d4128994ef29d8 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 25 Jul 2025 17:18:31 +0200 Subject: [PATCH] Delete debugging code Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 3 --- 1 file changed, 3 deletions(-) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index d008f2c..b799040 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -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₂ ... | 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 {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₃)