From 8772868f6b3796d6dd83a76ba2d0525388a71117 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 24 Jul 2018 16:35:19 -0400 Subject: Add ListUtil.{take,drop}_while --- src/Util/ListUtil.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'src/Util/ListUtil.v') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index f9e3457a1..3e0313800 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -331,6 +331,18 @@ Definition set_nth {T} n x (xs:list T) Definition splice_nth {T} n (x:T) xs := firstn n xs ++ x :: skipn (S n) xs. Hint Unfold splice_nth. +Fixpoint take_while {T} (f : T -> bool) (ls : list T) : list T + := match ls with + | nil => nil + | cons x xs => if f x then x :: @take_while T f xs else nil + end. + +Fixpoint drop_while {T} (f : T -> bool) (ls : list T) : list T + := match ls with + | nil => nil + | cons x xs => if f x then @drop_while T f xs else x :: xs + end. + Ltac boring := simpl; intuition auto with zarith datatypes; repeat match goal with -- cgit v1.2.3