Move Phead to List Base

anoma · Nov 8, 2024 · dbc3a55 · dbc3a55
1 parent 4485bd7
commit dbc3a55
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 5 deletions.
diff --git a/Stdlib/Data/List.juvix b/Stdlib/Data/List.juvix
@@ -16,11 +16,6 @@ import Stdlib.Trait.Foldable open using {
   fromPolymorphicFoldable;
 };
 
---- 𝒪(1). Partial function that returns the first element of a ;List;.
-phead {A} {{Partial}} : List A -> A
-  | (x :: _) := x
-  | nil := fail "head: empty list";
-
 instance
 eqListI {A} {{Eq A}} : Eq (List A) :=
   let

diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix
@@ -7,6 +7,7 @@ import Stdlib.Function open;
 import Stdlib.Data.Nat.Base open;
 import Stdlib.Data.Maybe.Base open;
 import Stdlib.Trait.Ord open;
+import Stdlib.Trait.Partial open;
 import Stdlib.Data.Pair.Base open;
 
 --- 𝒪(𝓃). Returns ;true; if the given object elem is in the ;List;.
@@ -165,6 +166,11 @@ head {A} (defaultValue : A) (list : List A) : A :=
     | x :: _ := x
     | nil := defaultValue;
 
+--- 𝒪(1). Partial function that returns the first element of a ;List;.
+phead {A} {{Partial}} : List A -> A
+  | (x :: _) := x
+  | nil := fail "head: empty list";
+
 syntax iterator any {init := 0; range := 1};
 
 --- 𝒪(𝓃). Returns ;true; if at least one element of the ;List; satisfies the predicate.