From: matitaweb Date: Wed, 29 Feb 2012 11:54:56 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~1926 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c57538d8f84e2e2d73bbda4b07570c10b1bf32a3;p=helm.git commit by user andrea --- diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma index 245a9fd3b..e699b626a 100644 --- a/weblib/basics/list.ma +++ b/weblib/basics/list.ma @@ -104,7 +104,7 @@ definition filter ≝ a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a T (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T) (λx,l0.if (p x) then (xa title="cons" href="cic:/fakeuri.def(1)":/a:l0) else l0) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a T). definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2. - a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a ?? (λi,acc.(a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? (f i) l2)a title="append" href="cic:/fakeuri.def(1)"@/aacc) a title="nil" href="cic:/fakeuri.def(1)"[/a ] l1. + a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a ?? (λi,acc.(a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? (f i) l2)a title="append" href="cic:/fakeuri.def(1)"@/aacc) a title="nil" href="cic:/fakeuri.def(1)"[/a ] l1. lemma filter_true : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a a title="cons" href="cic:/fakeuri.def(1)":/a: a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l.