michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

minor tweak

Browse source
This commit is contained in:
Jeremy Siek 2019-05-06 15:19:40 +02:00
parent 5070619dd9
commit 2e999b167e
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
extra/extra/CallByName.lagda
View file

@ -175,7 +175,7 @@ subst-subst {Γ}{Δ}{Σ}{ƛ N}{σ₁}{σ₂} = G
ƛ ((subst (exts σ₂)) ∘ (subst (exts σ₁))) N
≡⟨ cong ƛ_ (subst-subst{M = N}{σ₁ = exts σ₁}{σ₂ = exts σ₂}) ⟩
ƛ subst ((subst (exts σ₂)) ∘ (exts σ₁)) N
≡⟨ cong ƛ_ (subst-equal{M = N} (λ {A}{x} → subst-exts{Γ}{Δ}{Σ}{A}{x})) ⟩
≡⟨ cong ƛ_ (subst-equal{M = N} (λ {A}{x} → subst-exts{x = x})) ⟩
(ƛ subst (exts ((subst σ₂) ∘ σ₁)) N)
∎
subst-subst {M = L · M} = cong₂ _·_ (subst-subst{M = L}) (subst-subst{M = M})