From bfe30601962a694fe872858fdd07a13c52cecef8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Sicard-Ram=C3=ADrez?= <asr@eafit.edu.co>
Date: Wed, 10 Feb 2021 10:13:07 -0500
Subject: [PATCH] Fixed typos in the grammar for inherited terms.
---
src/plfa/part2/Inference.lagda.md | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/plfa/part2/Inference.lagda.md b/src/plfa/part2/Inference.lagda.md
index 0000f9ed..5be2978f 100644
--- 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.