From 69b82b0f568dd840f05f6aa9902ee6dcd5df5cad Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 8 Mar 2022 18:49:39 +0000 Subject: Migrate to agda-stdlib-2.0-dev. --- src/Helium/Data/Pseudocode/Manipulate.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Helium/Data/Pseudocode') diff --git a/src/Helium/Data/Pseudocode/Manipulate.agda b/src/Helium/Data/Pseudocode/Manipulate.agda index 0ca5194..a5fe519 100644 --- a/src/Helium/Data/Pseudocode/Manipulate.agda +++ b/src/Helium/Data/Pseudocode/Manipulate.agda @@ -1240,10 +1240,10 @@ private e (Vec.allFin m) where - helper : ∀ {n m} k (f : ∀ {n : ℕ} e (i : Fin m) → ∃ λ e′ → callDepth e′ ℕ.≤ k ⊔ callDepth e) → ∀ e xs → callDepth (Vec.foldl (λ _ → Expression Γ ret) {n} (λ {n} e i → proj₁ (f {n} e i)) e xs) ℕ.≤ k ⊔ callDepth e + helper : ∀ {n m} k (f : ∀ e (i : Fin m) → ∃ λ e′ → callDepth e′ ℕ.≤ k ⊔ callDepth e) → ∀ e xs → callDepth (Vec.foldl′ {n = n} (λ e i → proj₁ (f e i)) e xs) ℕ.≤ k ⊔ callDepth e helper k f e [] = ℕₚ.m≤n⊔m k (callDepth e) helper k f e (x ∷ xs) = begin - callDepth (Vec.foldl _ (λ e i → proj₁ (f e i)) (proj₁ (f e x)) xs) + callDepth (Vec.foldl′ (λ e i → proj₁ (f e i)) (proj₁ (f e x)) xs) ≤⟨ helper k f (proj₁ (f e x)) xs ⟩ k ⊔ callDepth (proj₁ (f e x)) ≤⟨ ℕₚ.⊔-monoʳ-≤ k (proj₂ (f e x)) ⟩ -- cgit v1.2.3