Merge pull request #452 from mdimjasevic/prop-preserve-beta

Properties: fix an informal rule in the text for β-ƛ
2020-01-27 14:59:33 -06:00 · 2020-01-27 14:59:33 -06:00 · 83b8e6da00
commit 83b8e6da00
parent d7143136ef 495123979c
1 changed files with 2 additions and 2 deletions
--- a/src/plfa/part2/Properties.lagda.md
+++ b/src/plfa/part2/Properties.lagda.md
@ -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