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

Merge pull request #450 from mdimjasevic/prop-abs-ind

Browse source 
Properties: fix the inductive hypothesis for lambda abstraction
This commit is contained in:
Philip Wadler 2020-01-13 12:52:49 -03:00 committed by GitHub
commit d26fd33118
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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.