Ignore:
Timestamp:
Aug 31, 2012, 4:12:35 PM (8 years ago)
Author:
campbell
Message:

Move generic definitions from recent commit to appropriate places.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r2306 r2314  
    5858]
    5959qed.
     60
     61(* Boolean predicate version of All *)
     62
     63let rec all (A:Type[0]) (P:A → bool) (l:list A) on l : bool ≝
     64match l with
     65[ nil ⇒ true
     66| cons h t ⇒ P h ∧ all A P t
     67].
     68
     69lemma all_All : ∀A,P,l. bool_to_Prop (all A P l) ↔ All A (λa.bool_to_Prop (P a)) l.
     70#A #P #l elim l
     71[ % //
     72| #h #t * #IH #IH' %
     73  [ whd in ⊢ (?% → %); cases (P h) [ #p % /2/ | * ]
     74  | * #p #H whd in ⊢ (?%); >p /2/
     75  ]
     76] qed.
     77
    6078
    6179let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝
Note: See TracChangeset for help on using the changeset viewer.