From bc5b4b7d9ee71c1e2acdd9c14c8ef66127c9deeb Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 8 Apr 2024 00:16:10 -0700 Subject: [PATCH] Explicitly write metas for missing functions Signed-off-by: Danila Fedorin --- Language.agda | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Language.agda b/Language.agda index 2b078d9..3b593fc 100644 --- a/Language.agda +++ b/Language.agda @@ -134,7 +134,8 @@ module Graphs where (Mk-⊆ n₁ p₁@refl g₁[]≡g₂[] e∈g₁⇒e∈g₂) (Mk-⊆ n₂ p₂@refl g₂[]≡g₃[] e∈g₂⇒e∈g₃) = record { n = n₁ +ⁿ n₂ ; sg₂≡sg₁+n = +-assoc s₁ n₁ n₂ - -- ; g₁[]≡g₂[] = λ idx → 1 + ; g₁[]≡g₂[] = {!!} + ; e∈g₁⇒e∈g₂ = {!!} -- lookup ns₁ idx ≡ lookup (cast p₁ ns₂) (idx ↑ˡ n) -- by g₁[]≡g₂[] -- lookup (cast p₁ ns₂) (idx ↑ˡ n) ≡ lookup ns₂ (Fin.cast (sym p₁) (idx ↑ˡ n)) -- by lookup-cast₁