projects
/
coq-hetmet.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
794719a
)
add split_list to General.v
author
Adam Megacz
<megacz@cs.berkeley.edu>
Sat, 14 May 2011 03:30:01 +0000
(20:30 -0700)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Sat, 14 May 2011 03:30:01 +0000
(20:30 -0700)
src/General.v
patch
|
blob
|
history
diff --git
a/src/General.v
b/src/General.v
index
f97989d
..
5d19e9c
100644
(file)
--- 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 _ _ }.
Instance ListToString {T:Type}{tst:ToString T} : ToString (list T) :=
{ toString := @listToString _ _ }.
+
(*******************************************************************************)
(* Tree Flags *)
(*******************************************************************************)
(* 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.
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".
(* Uniques *)
Variable UniqSupply : Type. Extract Inlined Constant UniqSupply => "UniqSupply.UniqSupply".
Variable Unique : Type. Extract Inlined Constant Unique => "Unique.Unique".