From 557a088c78b9d6d2311014c8ed887a52b4cff641 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Sun, 26 Jan 2020 10:26:36 +0100 Subject: [PATCH] Properties: fix 'well-typed' according to issue #318 --- src/plfa/part2/Properties.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part2/Properties.lagda.md b/src/plfa/part2/Properties.lagda.md index 072368a2..c6b56e1f 100644 --- 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