minor text edit
This commit is contained in:
parent
2486155f3f
commit
8ffc49e929
1 changed files with 1 additions and 1 deletions
|
@ -675,7 +675,7 @@ the predecessor of the current argument) and one corresponding to the
|
|||
zero branch of the case. (The cases could be in either order.
|
||||
We put the successor case first to ease comparison with Church numerals.)
|
||||
|
||||
Here is the representation of naturals encoded with de Bruijn indexes:
|
||||
Here is the Scott representation of naturals encoded with de Bruijn indexes:
|
||||
```
|
||||
`zero : ∀ {Γ} → (Γ ⊢ ★)
|
||||
`zero = ƛ ƛ (# 0)
|
||||
|
|
Loading…
Reference in a new issue