From 2dc431121e91bb3bc544ab8c65d07835ce47b353 Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Tue, 7 Apr 2020 08:19:03 -0400 Subject: [PATCH] simplified D^c --- src/plfa/part3/Denotational.lagda.md | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md index 7cd28762..6d3f1185 100644 --- a/src/plfa/part3/Denotational.lagda.md +++ b/src/plfa/part3/Denotational.lagda.md @@ -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