From c57538d8f84e2e2d73bbda4b07570c10b1bf32a3 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 29 Feb 2012 11:54:56 +0000 Subject: [PATCH] commit by user andrea --- weblib/basics/list.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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. -- 2.39.2