 Timestamp:
 Jul 5, 2011, 5:53:11 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r998 r1057 8 8 example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed. 9 9 example not_implemented: False. cases daemon qed. 10 11 let rec map2_opt 12 (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C) 13 (left: list A) (right: list B) on left ≝ 14 match left with 15 [ nil ⇒ 16 match right with 17 [ nil ⇒ Some ? (nil C) 18  _ ⇒ None ? 19 ] 20  cons hd tl ⇒ 21 match right with 22 [ nil ⇒ None ? 23  cons hd' tl' ⇒ 24 match map2_opt A B C f tl tl' with 25 [ None ⇒ None ? 26  Some tail ⇒ Some ? (f hd hd' :: tail) 27 ] 28 ] 29 ]. 30 31 let rec map2 32 (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C) 33 (left: list A) (right: list B) (proof:  left  =  right ) on left ≝ 34 match left return λx.  x  =  right  → list C with 35 [ nil ⇒ 36 match right return λy.  []  =  y  → list C with 37 [ nil ⇒ λnil_prf. nil C 38  _ ⇒ λcons_absrd. ? 39 ] 40  cons hd tl ⇒ 41 match right return λy.  hd::tl  =  y  → list C with 42 [ nil ⇒ λnil_absrd. ? 43  cons hd' tl' ⇒ λcons_prf. (f hd hd') :: map2 A B C f tl tl' ? 44 ] 45 ] proof. 46 [1: normalize in cons_absrd; 47 destruct(cons_absrd) 48 2: normalize in nil_absrd; 49 destruct(nil_absrd) 50 3: normalize in cons_prf; 51 destruct(cons_prf) 52 assumption 53 ] 54 qed. 10 55 11 56 lemma eq_rect_Type0_r :
Note: See TracChangeset
for help on using the changeset viewer.