Fixed typos in the grammar for inherited terms.

2021-02-10 10:13:07 -05:00 · 2021-02-10 10:13:07 -05:00 · bfe3060196
commit bfe3060196
parent a95b36da45
1 changed files with 3 additions and 3 deletions
--- a/src/plfa/part2/Inference.lagda.md
+++ b/src/plfa/part2/Inference.lagda.md
@ -191,12 +191,12 @@ We can extract the grammar for terms from the above:
      M⁻ ↓ A                              switch to inherited

    L⁻, M⁻, N⁻ ::=                      terms with inherited type
-      ƛ x ⇒ N                             abstraction
+      ƛ x ⇒ N⁻                            abstraction
      `zero                               zero
      `suc M⁻                             successor
      case L⁺ [zero⇒ M⁻ |suc x ⇒ N⁻ ]     case
-      μ x ⇒ N                             fixpoint
-      M ↑                                 switch to synthesized
+      μ x ⇒ N⁻                            fixpoint
+      M⁺ ↑                                switch to synthesized

 We will formalise the above shortly.