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

Properties: fix the rendering of a highlighted expression by removing a line break in the expression

Browse source
This commit is contained in:
Marko Dimjašević 2020-06-06 21:04:25 +02:00
parent 47cb1433db
commit fed1bc2610
No known key found for this signature in database
GPG key ID: 565EE9641503F0AA
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 either loop forever, in which case evaluation does not terminate, or
we will eventually reach a value, which is guaranteed to be closed and 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 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 · Agda code that can compute for us the reduction sequence of `plus · two · two`,
two · two`, and its Church numeral variant. and its Church numeral variant.
(The development in this chapter was inspired by the corresponding (The development in this chapter was inspired by the corresponding
development in _Software Foundations_, Volume _Programming Language development in _Software Foundations_, Volume _Programming Language