From 5a92232f20931ebb060082d5236239c2d2061e17 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 19 Mar 2011 14:15:18 -0700 Subject: [PATCH] add mapleaves to General.v --- src/General.v | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/General.v b/src/General.v index ffd0d29..7aefcf0 100644 --- a/src/General.v +++ b/src/General.v @@ -301,6 +301,16 @@ Fixpoint unleaves'' {A:Type}(l:list ??A) : Tree ??A := | (a::b) => (unleaves'' b),,(T_Leaf a) end. +Lemma mapleaves {T:Type}(t:Tree ??T){Q}{f:T->Q} : leaves (mapOptionTree f t) = map f (leaves t). + induction t. + destruct a; auto. + simpl. + rewrite IHt1. + rewrite IHt2. + rewrite map_app. + auto. + Qed. + Fixpoint filter {T:Type}(l:list ??T) : list T := match l with | nil => nil -- 1.7.10.4