remove foldr (#357)

as requested in issue #282
IntersectMBO · Feb 9, 2024 · 625e8c6 · 625e8c6
1 parent 5398da5
commit 625e8c6
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/Ledger/TokenAlgebra.lagda b/src/Ledger/TokenAlgebra.lagda
@@ -65,7 +65,8 @@ record TokenAlgebra : Set₁ where
 \AgdaTarget{sumᵛ}
 \begin{code}
   sumᵛ : List Value → Value
-  sumᵛ = foldr _+ᵛ_ (inject 0)
+  sumᵛ [] = inject 0
+  sumᵛ (x ∷ l) = x + sumᵛ l
 \end{code}
 \end{AgdaAlign}
 \caption{Token algebras, used for multi-assets}