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

De Bruijn: fix a line-break in the middle of a markup (#526)

Browse source
This commit is contained in:
Marko Dimjašević 2020-10-05 17:14:00 +02:00 committed by GitHub
parent 47d08d71fb
commit a78889398d
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/DeBruijn.lagda.md
View file

@ -736,8 +736,8 @@ variable to avoid capture:
`` ƛ "z" ⇒ ` "z" · (` "x" · `zero) ``
Say the bound `"x"` has type `` `ℕ ⇒ `ℕ ``, the substituted
`"y"` has type `` `ℕ ``, and the free `"x"` also has type ``
`ℕ ⇒ `ℕ ``. Here is the example formalised:
`"y"` has type `` `ℕ ``, and the free `"x"` also has type `` `ℕ ⇒ `ℕ ``.
Here is the example formalised:
```
M₅ : ∅ , `ℕ ⇒ `ℕ , `ℕ ⊢ (`ℕ ⇒ `ℕ) ⇒ `ℕ
M₅ = ƛ # 0 · # 1