Changeset 1630 for src/utilities/lists.ma
 Timestamp:
 Dec 19, 2011, 2:48:36 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/lists.ma
r1628 r1630 1 1 include "basics/lists/list.ma". 2 3 lemma All_append : ∀A,P,l,r. All A P l → All A P r → All A P (l@r). 4 #A #P #l elim l 5 [ // 6  #hd #tl #IH #r * #H1 #H2 #H3 % // @IH // 7 ] qed. 2 8 3 9 (* An alternative form of All that can be easier to use sometimes. *) … … 32 38  #ha #ta #IH * [ //  #hb #tb #H * #H1 #H2 % [ @H @H1  @(IH … H2) @H ] ] 33 39 ] qed. 40 41 let rec map_All (A,B:Type[0]) (P:A → Prop) (f:∀a. P a → B) (l:list A) (H:All A P l) on l : list B ≝ 42 match l return λl. All A P l → ? with 43 [ nil ⇒ λ_. nil B 44  cons hd tl ⇒ λH. cons B (f hd (proj1 … H)) (map_All A B P f tl (proj2 … H)) 45 ] H. 46
Note: See TracChangeset
for help on using the changeset viewer.