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

Properties: fix the inductive hypothesis for lambda abstraction in the description of the proof of subst

Browse source
This commit is contained in:
Marko Dimjašević 2020-01-13 10:45:46 +01:00
parent a49205abd3
commit 776f10940d
No known key found for this signature in database
GPG key ID: 565EE9641503F0AA
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/plfa/part2/Properties.lagda.md
View file

@ -742,8 +742,8 @@ Now that naming is resolved, let's unpack the first three cases:
∅ ⊢ V ⦂ B
Γ , x ⦂ A , y ⦂ B ⊢ N ⦂ C
------------------------------------
Γ , x ⦂ A , y ⦂ B ⊢ N [ y := V ] ⦂ C
----------------------------
Γ , x ⦂ A ⊢ N [ y := V ] ⦂ C
The typing rule for abstractions then yields the required conclusion.