michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fix newline rendering in Quantifiers chapter (#498)

Browse source
This commit is contained in:
Matthew Healy 2020-08-19 19:44:36 +02:00 committed by GitHub
parent b87defd53d
commit a591bf8616
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/plfa/part1/Quantifiers.lagda.md
View file

@ -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 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 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 that `∀ (x : A) → B x` holds, and a term `M` of type `A`, the term `L M`
M` provides evidence that `B M` holds. In other words, evidence that 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 `∀ (x : A) → B x` holds is a function that converts a term `M` of type
`A` into evidence that `B M` holds. `A` into evidence that `B M` holds.