From fed1bc261047faddacc5f37a389ae0f70fb83e53 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Sat, 6 Jun 2020 21:04:25 +0200 Subject: [PATCH] Properties: fix the rendering of a highlighted expression by removing a line break in the expression --- src/plfa/part2/Properties.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/part2/Properties.lagda.md b/src/plfa/part2/Properties.lagda.md index 57f4178c..6ccc544c 100644 --- a/src/plfa/part2/Properties.lagda.md +++ b/src/plfa/part2/Properties.lagda.md @@ -74,8 +74,8 @@ other term will itself be closed and well typed. Repeat. We will either loop forever, in which case evaluation does not terminate, or we will eventually reach a value, which is guaranteed to be closed and of the same type as the original term. We will turn this recipe into -Agda code that can compute for us the reduction sequence of `plus · -two · two`, and its Church numeral variant. +Agda code that can compute for us the reduction sequence of `plus · two · two`, +and its Church numeral variant. (The development in this chapter was inspired by the corresponding development in _Software Foundations_, Volume _Programming Language