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

Remove whitespace errors

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-07-25 15:26:41 +02:00
parent 6243326665
commit 13eee93255
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Lattice/Builder.agda
View File

@ -807,7 +807,7 @@ pathMeet'-comm {Ls = add-via-greatest l ls} (inj₁ lv₁) (inj₂ p₂) = ≈-j
pathMeet'-comm {Ls = add-via-greatest l ls} (inj₂ p₁) (inj₁ lv₂) = ≈-just (eqPath'-refl ls p₁)
greatestPath-pathMeet'-identˡ : ∀ {a} (Ls : Layers a) (greatest : LayerGreatest (head Ls))
(p : Path' Ls) →
(p : Path' Ls) →
let pᵍ = greatestPath Ls greatest
in lift-≈ (eqPath' Ls) (pathMeet' Ls pᵍ p) (just p)
greatestPath-pathMeet'-identˡ (single (plt ∷⁺ []) ) (MkLayerGreatest {{hasGreatest = hasGreatest}}) (inj₁ v)
@ -822,7 +822,7 @@ greatestPath-pathMeet'-identˡ {a = a} (add-via-greatest (plt ∷⁺ []) ls) (Mk
greatestPath-pathMeet'-identˡ (add-via-greatest l ls) (MkLayerGreatest {{hasGreatest = hasGreatest}}) (inj₂ p) = ≈-just (eqPath'-refl ls p)
greatestPath-pathMeet'-identʳ : ∀ {a} (Ls : Layers a) (greatest : LayerGreatest (head Ls))
(p : Path' Ls) →
(p : Path' Ls) →
let pᵍ = greatestPath Ls greatest
in lift-≈ (eqPath' Ls) (pathMeet' Ls p pᵍ) (just p)
greatestPath-pathMeet'-identʳ Ls greatest p