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

simplified D^c

Browse source
This commit is contained in:
Jeremy Siek 2020-04-07 08:19:03 -04:00
parent 3ab180ad8d
commit 2dc431121e
1 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/plfa/part3/Denotational.lagda.md
View file

@ -539,9 +539,7 @@ for a given path.
```
Dᶜ : (n : ℕ) → Vec Value (suc n) → Value
Dᶜ zero (a[0] ∷ []) = ⊥ ↦ a[0] ↦ a[0]
Dᶜ (suc n) (a[n+1] ∷ a[n] ∷ ls) =
(D^suc (suc n) (a[n+1] ∷ a[n] ∷ ls)) ↦ (vec-last (a[n] ∷ ls)) ↦ a[n+1]
Dᶜ n (a[n] ∷ ls) = (D^suc n (a[n] ∷ ls)) ↦ (vec-last (a[n] ∷ ls)) ↦ a[n]
```
* The Church numeral for 0 ignores its first argument and returns