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

Properties: fixes an informal rule in the text for β-ƛ by using a reduction relation instead of the typing judgment

Browse source
This commit is contained in:
Marko Dimjašević 2020-01-22 22:28:05 +01:00
parent 00bd32e7ac
commit 495123979c
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

@ -841,8 +841,8 @@ Let's unpack the cases for two of the reduction rules:
* Rule `β-ƛ`. We have
Value V
----------------------------
(ƛ x ⇒ N) · V ⊢ N [ x := V ]
-----------------------------
(ƛ x ⇒ N) · V —→ N [ x := V ]
where the left-hand side is typed by