Skip to content

Commit 644890d

Browse files
committed
Removed unused function list_init
1 parent 15ea240 commit 644890d

File tree

1 file changed

+0
-7
lines changed

1 file changed

+0
-7
lines changed

theories/Common/Utils.v

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -19,13 +19,6 @@ Local Open Scope Z_scope.
1919
Local Open Scope bool_scope.
2020

2121

22-
Fixpoint list_init {A:Type} (n:nat) (f:nat -> A): list A
23-
:=
24-
match n with
25-
| O => []
26-
| S n => (f n) :: list_init n f
27-
end.
28-
2922
(** Inlike OCaml version if lists have different sizes, we just terminate
3023
after consuming the shortest one, without signaling error *)
3124
Fixpoint fold_left2 {A B C:Type} (f: A -> B -> C -> A) (accu:A) (l1:list B) (l2:list C): A :=

0 commit comments

Comments
 (0)