From 06ef4b8d0206389472bfdfeb38972d2b838e2852 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 19 Mar 2011 14:15:11 -0700 Subject: [PATCH] add itmap and itree_to_tree --- src/General.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/General.v b/src/General.v index e1e5791..188a2dc 100644 --- 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 ]. +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. (*******************************************************************************) -- 1.7.10.4