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

Merge pull request #477 from mdimjasevic/prop-line-break

Browse source 
Properties: fix the rendering of a highlighted expression
This commit is contained in:
Philip Wadler 2020-06-07 10:23:55 +01:00 committed by GitHub
commit 2b0f229c93
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/part2/Properties.lagda.md
View file

@ -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