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

[ fix ] inline code block

Browse source
This commit is contained in:
AD1024 2019-09-30 01:13:14 -07:00
parent a79cd54db3
commit 4d919d75e5
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/plfa/part2/Lambda.lagda.md
View file

@ -238,7 +238,7 @@ C-c C-n to normalise the term
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