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

substZero

Browse source
This commit is contained in:
Jeremy Siek 2020-03-25 15:42:33 -04:00
parent 8ef93f790b
commit 724ec85423
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/plfa/part2/More.lagda.md
View file

@ -785,16 +785,16 @@ subst σ (case× L M) = case× (subst σ L) (subst (exts (exts σ)) M)
## Single and double substitution ## Single and double substitution
``` ```
substZero : ∀ {Γ}{A B} → Γ ⊢ A → Γ , A ∋ B → Γ ⊢ B
substZero V Z = V
substZero V (S x) = ` x
_[_] : ∀ {Γ A B} _[_] : ∀ {Γ A B}
→ Γ , A ⊢ B → Γ , A ⊢ B
→ Γ ⊢ A → Γ ⊢ A
--------- ---------
→ Γ ⊢ B → Γ ⊢ B
_[_] {Γ} {A} N V = subst {Γ , A} {Γ} σ N _[_] {Γ} {A} N V = subst {Γ , A} {Γ} (substZero V) N
where
σ : ∀ {B} → Γ , A ∋ B → Γ ⊢ B
σ Z = V
σ (S x) = ` x
_[_][_] : ∀ {Γ A B C} _[_][_] : ∀ {Γ A B C}
→ Γ , A , B ⊢ C → Γ , A , B ⊢ C