File tree Expand file tree Collapse file tree 2 files changed +6
-5
lines changed Expand file tree Collapse file tree 2 files changed +6
-5
lines changed Original file line number Diff line number Diff line change @@ -16,11 +16,6 @@ import Stdlib.Trait.Foldable open using {
16
16
fromPolymorphicFoldable;
17
17
};
18
18
19
- --- πͺ(1). Partial function that returns the first element of a ;List;.
20
- phead {A} {{Partial}} : List A -> A
21
- | (x :: _) := x
22
- | nil := fail "head: empty list";
23
-
24
19
instance
25
20
eqListI {A} {{Eq A}} : Eq (List A) :=
26
21
let
Original file line number Diff line number Diff line change @@ -7,6 +7,7 @@ import Stdlib.Function open;
7
7
import Stdlib.Data.Nat.Base open;
8
8
import Stdlib.Data.Maybe.Base open;
9
9
import Stdlib.Trait.Ord open;
10
+ import Stdlib.Trait.Partial open;
10
11
import Stdlib.Data.Pair.Base open;
11
12
12
13
--- πͺ(π). Returns ;true; if the given object elem is in the ;List;.
@@ -165,6 +166,11 @@ head {A} (defaultValue : A) (list : List A) : A :=
165
166
| x :: _ := x
166
167
| nil := defaultValue;
167
168
169
+ --- πͺ(1). Partial function that returns the first element of a ;List;.
170
+ phead {A} {{Partial}} : List A -> A
171
+ | (x :: _) := x
172
+ | nil := fail "head: empty list";
173
+
168
174
syntax iterator any {init := 0; range := 1};
169
175
170
176
--- πͺ(π). Returns ;true; if at least one element of the ;List; satisfies the predicate.
You canβt perform that action at this time.
0 commit comments