Properties: fix 'well-typed' according to issue #318

2020-01-26 10:26:36 +01:00 · 2020-01-26 10:26:36 +01:00 · 557a088c78
commit 557a088c78
parent 00bd32e7ac
1 changed files with 1 additions and 1 deletions
--- a/src/plfa/part2/Properties.lagda.md
+++ b/src/plfa/part2/Properties.lagda.md
@ -967,7 +967,7 @@ remaining.  There are two possibilities:

  + Term `L` is a value, so we are done. We return the
    trivial reduction sequence `L —↠ L`, evidence that `L` is
-    well-typed, and the evidence that `L` is a value.
+    well typed, and the evidence that `L` is a value.

  + Term `L` steps to another term `M`.  Preservation provides
    evidence that `M` is also well typed, and we recursively invoke