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

fit to available space

Browse source
This commit is contained in:
Philip Wadler 2017-07-12 15:52:31 +01:00
parent a2940a3b12
commit 2f1f78d8b3
2 changed files with 2252 additions and 2248 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4492
out/StlcProp.md
View file

File diff suppressed because it is too large Load diff

8
src/StlcProp.lagda
View file

@ -394,11 +394,13 @@ context-lemma {Γ} {Γ′} {λ[ x ∶ A ] N} Γ~Γ′ (⇒-I ⊢N) = ⇒-I (cont
Γx~Γ′x {y} y∈N with x ≟ y
... | yes refl = refl
... | no x≢y = Γ~Γ′ (free-λ x≢y y∈N)
context-lemma Γ~Γ′ (⇒-E ⊢L ⊢M) = ⇒-E (context-lemma (Γ~Γ′ ∘ free-·₁) ⊢L) (context-lemma (Γ~Γ′ ∘ free-·₂) ⊢M)
context-lemma Γ~Γ′ (⇒-E ⊢L ⊢M) = ⇒-E (context-lemma (Γ~Γ′ ∘ free-·₁) ⊢L)
(context-lemma (Γ~Γ′ ∘ free-·₂) ⊢M)
context-lemma Γ~Γ′ 𝔹-I₁ = 𝔹-I₁
context-lemma Γ~Γ′ 𝔹-I₂ = 𝔹-I₂
context-lemma Γ~Γ′ (𝔹-E ⊢L ⊢M ⊢N)
= 𝔹-E (context-lemma (Γ~Γ′ ∘ free-if₁) ⊢L) (context-lemma (Γ~Γ′ ∘ free-if₂) ⊢M) (context-lemma (Γ~Γ′ ∘ free-if₃) ⊢N)
context-lemma Γ~Γ′ (𝔹-E ⊢L ⊢M ⊢N) = 𝔹-E (context-lemma (Γ~Γ′ ∘ free-if₁) ⊢L)
(context-lemma (Γ~Γ′ ∘ free-if₂) ⊢M)
(context-lemma (Γ~Γ′ ∘ free-if₃) ⊢N)
\end{code}