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

Explicitly write metas for missing functions

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-04-08 00:16:10 -07:00
parent 520b2b514c
commit bc5b4b7d9e
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Language.agda
View File

@ -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 (Mk-⊆ n₁ p₁@refl g₁[]≡g₂[] e∈g₁⇒e∈g₂) (Mk-⊆ n₂ p₂@refl g₂[]≡g₃[] e∈g₂⇒e∈g₃) = record
{ n = n₁ +ⁿ n₂ { n = n₁ +ⁿ n₂
; sg₂≡sg₁+n = +-assoc s₁ 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 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₁ -- lookup (cast p₁ ns₂) (idx ↑ˡ n) ≡ lookup ns₂ (Fin.cast (sym p₁) (idx ↑ˡ n)) -- by lookup-cast₁