From 3e2719d45fb3157f318d394431ebc470083ce47f Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 8 Apr 2024 22:45:04 -0700 Subject: [PATCH] Turn old proof into a hole to clean up later. Signed-off-by: Danila Fedorin --- Language.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Language.agda b/Language.agda index e769597..979fcec 100644 --- a/Language.agda +++ b/Language.agda @@ -228,7 +228,7 @@ module Graphs where , record { n = 1 ; sg₂≡sg₁+n = refl - ; g₁[]≡g₂[] = λ idx → trans (sym (lookup-++ˡ (Graph.nodes g) (bss ∷ []) idx)) (sym (cong (λ vec → lookup vec (idx ↑ˡ 1)) (cast-is-id refl (Graph.nodes g ++ (bss ∷ []))))) + ; g₁[]≡g₂[] = {!!} -- λ idx → trans (sym (lookup-++ˡ (Graph.nodes g) (bss ∷ []) idx)) (sym (cong (λ vec → lookup vec (idx ↑ˡ 1)) (cast-is-id refl (Graph.nodes g ++ (bss ∷ []))))) ; e∈g₁⇒e∈g₂ = λ e∈g₁ → x∈xs⇒fx∈fxs (λ e' → ↑ˡ-Edge e' 1) e∈g₁ } )