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

Lambda: fix indentation for correct rendering

Browse source
This commit is contained in:
Marko Dimjašević 2019-12-29 22:37:49 +01:00
parent 5547b5251e
commit ed97783252
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/Lambda.lagda.md
View file

@ -234,11 +234,11 @@ We intend to apply the function only when the first term is a variable, which we
indicate by postulating a term `impossible` of the empty type `⊥`. If we use
C-c C-n to normalise the term
ƛ′ two ⇒ two
ƛ′ two ⇒ two
Agda will return an answer warning us that the impossible has occurred:
⊥-elim (plfa.part2.Lambda.impossible (`` `suc (`suc `zero)) (`suc (`suc `zero)) ``)
⊥-elim (plfa.part2.Lambda.impossible (`` `suc (`suc `zero)) (`suc (`suc `zero)) ``)
While postulating the impossible is a useful technique, it must be
used with care, since such postulation could allow us to provide