Changeset 1059 for src/ASM/Util.ma
 Timestamp:
 Jul 6, 2011, 6:09:39 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r1057 r1059 8 8 example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed. 9 9 example not_implemented: False. cases daemon qed. 10 10 11 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" 12 with precedence 10 13 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }. 14 15 let rec reduce 16 (A: Type[0]) (left: list A) (right: list A) on left ≝ 17 match left with 18 [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉 19  cons hd tl ⇒ 20 match right with 21 [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉 22  cons hd' tl' ⇒ 23 let 〈cleft, cright〉 ≝ reduce A tl tl' in 24 let 〈commonl, restl〉 ≝ cleft in 25 let 〈commonr, restr〉 ≝ cright in 26 〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉 27 ] 28 ]. 29 30 (* 31 let rec reduce_strong 32 (A: Type[0]) (left: list A) (right: list A) (prf:  left  =  right ) on left ≝ 33 match left return λx. x = right → Σret: ((list A) × (list A)) × ((list A) × (list A)).  \fst (\fst ret)  =  \fst (\snd ret)  with 34 [ nil ⇒ 35 match right return λy.  [ ]  =  y  → Σret: ((list A) × (list A)) × ((list A) × (list A)).  \fst (\fst ret)  =  \fst (\snd ret)  with 36 [ nil ⇒ λnil_nil_prf. dp ? 〈〈[ ], [ ]〉, 〈[ ], [ ]〉〉 ? 37  cons hd tl ⇒ λnil_cons_asrd_prf. ? 38 ] 39  cons hd tl ⇒ 40 match right return λy.  hd::tl  =  y  → Σret: ((list A) × (list A)) × ((list A) × (list A)).  \fst (\fst ret)  =  \fst (\snd ret)  with 41 [ nil ⇒ λcons_nil_absrd_prf. ? 42  cons hd' tl' ⇒ λcons_cons_prf. ? 43 ] 44 ] prf. 45 *) 46 47 axiom reduce_length: 48 ∀A: Type[0]. 49 ∀left, right: list A. 50 ∀prf:  left  =  right . 51 \fst (\fst (reduce A left right)) = \fst (\snd (reduce A left right)). 52 11 53 let rec map2_opt 12 54 (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C) … … 255 297  S o ⇒ f (iterate A f a o) 256 298 ]. 257 258 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"259 with precedence 10260 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.261 299 262 300 (* Yeah, I probably ought to do something more general... *)
Note: See TracChangeset
for help on using the changeset viewer.