Slightly format some code
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
da2f7f51d7
commit
57606636a7
|
@ -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))
|
||||
}
|
||||
)
|
||||
|
||||
|
|
Loading…
Reference in New Issue
Block a user