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:
75ce56c
)
General: add ilist_ins
author
Adam Megacz
<megacz@cs.berkeley.edu>
Mon, 11 Jul 2011 05:04:16 +0000
(22:04 -0700)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Mon, 29 Aug 2011 23:17:40 +0000
(16:17 -0700)
src/General.v
patch
|
blob
|
history
diff --git
a/src/General.v
b/src/General.v
index
53e3753
..
541dc6f
100644
(file)
--- a/
src/General.v
+++ b/
src/General.v
@@
-912,6
+912,19
@@
Lemma ilist_app {T}{F}{l1:list T}(v1:IList T F l1) : forall {l2:list T}(v2:IList
apply IHl1; auto.
Defined.
apply IHl1; auto.
Defined.
+Definition ilist_ins {T}{F}{l:list T} z (fz:F z) : forall n (il:IList T F l), IList T F (list_ins n z l).
+ induction l; simpl.
+ intros.
+ destruct n; simpl.
+ apply ICons; [ apply fz | apply INil ].
+ apply ICons; [ apply fz | apply INil ].
+ intros.
+ destruct n; simpl.
+ apply ICons; auto.
+ inversion il; subst.
+ apply ICons; auto.
+ Defined.
+
Fixpoint ilist_to_list {T}{Z}{l:list T}(il:IList T (fun _ => Z) l) : list Z :=
match il with
| INil => nil
Fixpoint ilist_to_list {T}{Z}{l:list T}(il:IList T (fun _ => Z) l) : list Z :=
match il with
| INil => nil