bug: restored deleted Nat operations

agda · Jan 22, 2025 · 7eb7626 · 7eb7626
1 parent c75b172
commit 7eb7626
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
@@ -150,6 +150,12 @@ null : List A → Bool
 null []       = true
 null (x ∷ xs) = false
 
+sum : List ℕ → ℕ
+sum = foldr _+_ 0
+
+product : List ℕ → ℕ
+product = foldr _*_ 1
+
 length : List A → ℕ
 length = foldr (const suc) 0