Changeset 2335 for src/common/PositiveMap.ma
 Timestamp:
 Sep 20, 2012, 6:57:34 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/PositiveMap.ma
r2307 r2335 567 567 ] qed. 568 568 569 569 (* An "informative" dependently typed fold *) 570 571 let rec pm_fold_inf_aux 572 (A, B: Type[0]) 573 (t: positive_map A) 574 (f: ∀p:Pos. ∀a:A. lookup_opt … p t = Some A a → B → B) 575 (t': positive_map A) 576 (pre: Pos → Pos) 577 (b: B) on t': (∀p. lookup_opt … p t' = lookup_opt … (pre p) t) → B ≝ 578 match t' return λt'. (∀p. lookup_opt A p t' = lookup_opt A (pre p) t) → B with 579 [ pm_leaf ⇒ λ_. b 580  pm_node a l r ⇒ λH. 581 let b ≝ match a return λa. lookup_opt A one (pm_node A a ??) = ? → B with [ None ⇒ λ_.b  Some a ⇒ λH. f (pre one) a ? b ] (H one) in 582 let b ≝ pm_fold_inf_aux A B t f l (λx. pre (p0 x)) b ? in 583 pm_fold_inf_aux A B t f r (λx. pre (p1 x)) b ? 584 ]. 585 [ #p @(H (p1 p))  #p @(H (p0 p))  <H % ] 586 qed. 587 588 definition pm_fold_inf : ∀A, B: Type[0]. ∀t: positive_map A. 589 ∀f: (∀p:Pos. ∀a:A. lookup_opt … p t = Some A a → B → B). B → B ≝ 590 λA,B,t,f,b. pm_fold_inf_aux A B t f t (λx.x) b (λp. refl ??). 591
Note: See TracChangeset
for help on using the changeset viewer.