From e1c9b2e7a28fabb4c0a9ce3cbd4d2ae099d60b5a Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 13 May 2011 20:30:01 -0700 Subject: [PATCH 1/1] add split_list to General.v --- src/General.v | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/General.v b/src/General.v index f97989d..5d19e9c 100644 --- a/src/General.v +++ b/src/General.v @@ -478,6 +478,7 @@ Fixpoint listToString {T:Type}{tst:ToString T}(l:list T) : string := Instance ListToString {T:Type}{tst:ToString T} : ToString (list T) := { toString := @listToString _ _ }. + (*******************************************************************************) (* Tree Flags *) @@ -952,6 +953,16 @@ Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???( apply (Error (error_message (length l) n)). Defined. +(* this makes a type function application, ensuring not to oversaturate it (though if it was undersaturated we can't fix that) *) +Fixpoint split_list {T}(l:list T)(n:nat) : ???(list T * list T) := + match n with + | O => OK (nil , l) + | S n' => match l with + | nil => Error "take_list failed" + | h::t => split_list t n' >>= fun t' => let (t1,t2) := t' in OK ((h::t1),t2) + end + end. + (* Uniques *) Variable UniqSupply : Type. Extract Inlined Constant UniqSupply => "UniqSupply.UniqSupply". Variable Unique : Type. Extract Inlined Constant Unique => "Unique.Unique". -- 1.7.10.4