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

minor fixes

Browse source
This commit is contained in:
wadler 2018-06-30 22:26:50 -03:00
parent 9f8c8ba57e
commit ec049e109a
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/plta/DeBruijn.lagda
View file

@ -558,13 +558,13 @@ subst : ∀ {Γ Δ}
→ (∀ {A} → Γ ∋ A → Δ ⊢ A) → (∀ {A} → Γ ∋ A → Δ ⊢ A)
------------------------ ------------------------
→ (∀ {A} → Γ ⊢ A → Δ ⊢ A) → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
subst σ (` k) = σ k subst σ (` k) = σ k
subst σ (ƛ N) = ƛ (subst (exts σ) N) subst σ (ƛ N) = ƛ (subst (exts σ) N)
subst σ (L · M) = (subst σ L) · (subst σ M) subst σ (L · M) = (subst σ L) · (subst σ M)
subst σ (`zero) = `zero subst σ (`zero) = `zero
subst σ (`suc M) = `suc (subst σ M) subst σ (`suc M) = `suc (subst σ M)
subst σ (`case L M N) = `case (subst σ L) (subst σ M) (subst (exts σ) N) subst σ (`case L M N) = `case (subst σ L) (subst σ M) (subst (exts σ) N)
subst σ (μ N) = μ (subst (exts σ) N) subst σ (μ N) = μ (subst (exts σ) N)
_[_] : ∀ {Γ A B} _[_] : ∀ {Γ A B}
→ Γ , A ⊢ B → Γ , A ⊢ B