Merge pull request #457 from mdimjasevic/prop-well-typed-2

Properties: fix 'well-typed' according to issue #318
2020-01-26 13:23:55 -06:00 · 2020-01-26 13:23:55 -06:00 · 0e5a71ec1e
commit 0e5a71ec1e
parent 00bd32e7ac 557a088c78
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