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

Merge pull request #418 from AD1024/dev

Browse source 
[ fix ] inline code block
This commit is contained in:
Wen Kokke 2019-09-30 13:33:00 +01:00 • committed by GitHub
commit 7a3ba37659
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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