From 625e8c6f53c7496524363263936c3239ca58da31 Mon Sep 17 00:00:00 2001
From: William DeMeo <williamdemeo@gmail.com>
Date: Fri, 9 Feb 2024 11:14:49 -0700
Subject: [PATCH] remove foldr (#357)

as requested in issue #282
---
 src/Ledger/TokenAlgebra.lagda | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Ledger/TokenAlgebra.lagda b/src/Ledger/TokenAlgebra.lagda
index ad926ef4f..a12794457 100644
--- 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}