projects
/
coq-hetmet.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
30cc675
)
add itmap and itree_to_tree
author
Adam Megacz
<megacz@cs.berkeley.edu>
Sat, 19 Mar 2011 21:15:11 +0000
(14:15 -0700)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Sat, 19 Mar 2011 21:15:11 +0000
(14:15 -0700)
src/General.v
patch
|
blob
|
history
diff --git
a/src/General.v
b/src/General.v
index
e1e5791
..
188a2dc
100644
(file)
--- a/
src/General.v
+++ b/
src/General.v
@@
-589,7
+589,22
@@
Implicit Arguments INil [ I F ].
Implicit Arguments ILeaf [ I F ].
Implicit Arguments IBranch [ I F ].
Implicit Arguments ILeaf [ I F ].
Implicit Arguments IBranch [ I F ].
+Definition itmap {I}{F}{G}{il:Tree ??I}(f:forall i:I, F i -> G i) : ITree I F il -> ITree I G il.
+ induction il; intros; auto.
+ destruct a.
+ apply ILeaf.
+ apply f.
+ inversion X; auto.
+ apply INone.
+ apply IBranch; inversion X; auto.
+ Defined.
+Fixpoint itree_to_tree {T}{Z}{l:Tree ??T}(il:ITree T (fun _ => Z) l) : Tree ??Z :=
+ match il with
+ | INone => []
+ | ILeaf _ a => [a]
+ | IBranch _ _ b1 b2 => (itree_to_tree b1),,(itree_to_tree b2)
+ end.
(*******************************************************************************)
(*******************************************************************************)