 Timestamp:
 Nov 24, 2011, 11:52:52 AM (9 years ago)
 Location:
 src
 Files:

 1 added
 2 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/lists.ma
r1516 r1551 129 129 definition position_of: ∀A:Type[0]. (A → bool) → list A → option nat ≝ 130 130 λA,found,l. position_of_aux A found l 0. 131 132 133 let rec make_list (A:Type[0]) (a:A) (n:nat) on n : list A ≝ 134 match n with 135 [ O ⇒ [ ] 136  S m ⇒ a::(make_list A a m) 137 ]. 
src/utilities/option.ma
r1316 r1551 16 16 ] qed. 17 17 18 definition option_map_def : ∀A,B:Type[0]. (A → B) → B → option A → B ≝ 19 λA,B,f,d,o. match o with [ None ⇒ d  Some a ⇒ f a ]. 20 18 21 lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → False. 19 22 (∀v. x = Some ? v → Q (P v)) →
Note: See TracChangeset
for help on using the changeset viewer.