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

stuck at two places in proof of preservation of substitution

Browse source
This commit is contained in:
wadler 2017-06-25 19:09:39 +01:00
parent 500d56b3b0
commit fbd3cc1d2e
1 changed files with 0 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/StlcProp.lagda
View file

@ -490,12 +490,6 @@ weaken-closed {P} {A} {Γ} ⊢P = weaken g ⊢P
{- {-
[:=]-preserves-⊢ {x} ⊢P (Ax {_} {y} Γy≡justB) with x ≟ y
... | yes x=y = ?
... | no x≠y = ?
[:=]-preserves-⊢ {Γ} {x} v∶A (var y y∈Γ) with x ≟ y [:=]-preserves-⊢ {Γ} {x} v∶A (var y y∈Γ) with x ≟ y
... | yes x=y = {!!} ... | yes x=y = {!!}
... | no x≠y = {!!} ... | no x≠y = {!!}