Changeset 1630 for src/utilities


Ignore:
Timestamp:
Dec 19, 2011, 2:48:36 PM (8 years ago)
Author:
campbell
Message:

Remainder of freshness in Clight to Cminor pass.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r1628 r1630  
    11include "basics/lists/list.ma".
     2
     3lemma 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.
    28
    39(* An alternative form of All that can be easier to use sometimes. *)
     
    3238| #ha #ta #IH * [ // | #hb #tb #H * #H1 #H2 % [ @H @H1 | @(IH … H2) @H ] ]
    3339] qed.
     40
     41let 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 ≝
     42match 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.