lude

commit ba7503faee0f37511fe96c3f1cf1b0379a30526c
parent b40f468c8ea5209a59a422eb9ecb9ab26f92794f
Author: Robert Russell <robert@rr3.xyz>
Date:   Fri, 16 Oct 2026 10:16:02 -0700

List: add index

Diffstat:
M
src/Lude/List.hs
 | 
18
++++++++++++++++++

1 file changed, 18 insertions(+), 0 deletions(-)
diff --git a/src/Lude/List.hs b/src/Lude/List.hs
@@ -1,7 +1,25 @@
 module Lude.List (
     List,
+    index,
+    ( #? ),
 ) where
 
+import Lude.Haskell
 import Lude.Haskell.List (List)
+import Lude.Maybe
+import Lude.Natural
+
+-- import Lude.Algebra.Magma
+
+-- TODO: pindex, (!!) :: (Partial) => ...
+
+-- TODO: Somehow generalize indices beyond Natural (e.g., Nat64 should also work?)
 
 --------------------------------------------------------------------------------
+
+index, ( #? ) :: forall (a :: Type). List a -> Natural -> Maybe a
+index [] _ = Nothing
+index (h : _) NaturalZero = Just h
+index (_ : t) (NaturalSucc n) = index t n
+( #? ) = index
+infixl 9 #?