From 57606636a7a1ab0f04664137cf5467711bd623f8 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 12 Apr 2024 23:22:31 -0700 Subject: [PATCH] Slightly format some code Signed-off-by: Danila Fedorin --- Language.agda | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Language.agda b/Language.agda index 473d218..b23e4a5 100644 --- a/Language.agda +++ b/Language.agda @@ -269,7 +269,9 @@ module Graphs where ; nsg₂≡nsg₁++newNodes = cast-sym _ (++-identityʳ (+-comm s 0) ns) ; e∈g₁⇒e∈g₂ = λ {e} e∈es → cast∈⇒∈subst (+-comm s 0) (+-comm 0 s) _ _ - (subst (λ e' → e' ∈ˡ _) (↑ˡ-Edge-identityʳ e (+-comm s 0)) (∈ˡ-++⁺ʳ es' e∈es)) + (subst (λ e' → e' ∈ˡ _) + (↑ˡ-Edge-identityʳ e (+-comm s 0)) + (∈ˡ-++⁺ʳ es' e∈es)) } )