From a591bf8616622ebb879b58f480d66dc228cf5be6 Mon Sep 17 00:00:00 2001 From: Matthew Healy Date: Wed, 19 Aug 2020 19:44:36 +0200 Subject: [PATCH] Fix newline rendering in Quantifiers chapter (#498) --- src/plfa/part1/Quantifiers.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/part1/Quantifiers.lagda.md b/src/plfa/part1/Quantifiers.lagda.md index 7d4ccfc0..ba18f34a 100644 --- a/src/plfa/part1/Quantifiers.lagda.md +++ b/src/plfa/part1/Quantifiers.lagda.md @@ -51,8 +51,8 @@ Evidence that `∀ (x : A) → B x` holds is of the form where `N x` is a term of type `B x`, and `N x` and `B x` both contain a free variable `x` of type `A`. Given a term `L` providing evidence -that `∀ (x : A) → B x` holds, and a term `M` of type `A`, the term `L -M` provides evidence that `B M` holds. In other words, evidence that +that `∀ (x : A) → B x` holds, and a term `M` of type `A`, the term `L M` +provides evidence that `B M` holds. In other words, evidence that `∀ (x : A) → B x` holds is a function that converts a term `M` of type `A` into evidence that `B M` holds.