diff --git a/source/Scrolls/BouncingScroll.mmt b/source/Scrolls/BouncingScroll.mmt index 9f136cc8e1d95a862d40bd7607169cc45a9c18ed..16622f78ae6b0b595f6e782d0de17f1e4b76ab7e 100644 --- a/source/Scrolls/BouncingScroll.mmt +++ b/source/Scrolls/BouncingScroll.mmt @@ -27,14 +27,10 @@ theory BouncingScroll = ⟨(Ï€l (Ï€r (Ï€r vals))), new_ht (Ï€r (Ï€r (Ï€l (Ï€r vals)))) (Ï€l (Ï€r (Ï€r vals))) (Ï€l (Ï€r (Ï€r (Ï€r vals)))) (Ï€r (Ï€r (Ï€r (Ï€r vals)))), (Ï€r (Ï€r (Ï€r (Ï€r vals))))⟩⟩ â™ - red_ht_helper : ((℠× ℠× â„) × (℠× ℠× â„) × (℠× ℠× â„)) ⟶ ℠☠= + red_ht : ((℠× ℠× â„) × (℠× ℠× â„) × (℠× ℠× â„)) ⟶ ℠☠= [cele] Ï€l (Ï€r (Ï€r (Ï€r cele))) â™ - red_ht : List[(℠× ℠× â„) × (℠× ℠× â„) × (℠× ℠× â„)] ⟶ List[â„] ☠= - [clsele] clsele map ([xele] red_ht_helper xele) â™ get_pos_fun: ℠⟶ ℠⟶ ℠⟶ ℠⟶ ℠⟶ ℠⟶ ℠⟶ (℠⟶ (℠× ℠× â„)) ☠= [x,y,z,xv,yv,zv,g] ([t] ⟨plus_real_lit x (times_real_lit xv t), plus_real_lit y (times_real_lit yv t), plus_real_lit (times_real_lit (times_real_lit 0.5 g) (times_real_lit t t)) (plus_real_lit z (times_real_lit zv t))⟩ ) â™ - red_funcs : List[(℠× ℠× â„) × (℠× ℠× â„) × (℠× ℠× â„)] ⟶ List[℠⟶ (℠× ℠× â„)] ☠= - [cls] (cls map ([vals] get_pos_fun (Ï€l (Ï€l vals)) (Ï€l (Ï€r (Ï€l vals))) (Ï€r (Ï€r (Ï€l vals))) (Ï€l (Ï€l (Ï€r vals))) (Ï€l (Ï€r (Ï€l (Ï€r vals)))) (Ï€r (Ï€r (Ï€l (Ï€r vals)))) (Ï€l (Ï€r (Ï€r vals))))) ++ nil â™ end_cond : ((℠× ℠× â„) × (℠× ℠× â„) × (℠× ℠× â„)) ⟶ bool ☠= [vals] leq_real_lit (Ï€l (Ï€r (Ï€r (Ï€r vals)))) 0.1 â™ âš @@ -55,10 +51,8 @@ theory BouncingScroll = theory Solution = include ?BouncingScroll/Problem â™ full_list: List[(℠× ℠× â„) × (℠× ℠× â„) × (℠× ℠× â„)] ☠= stepUntil ((℠× ℠× â„) × (℠× ℠× â„) × (℠× ℠× â„)) (prep xposition yposition zposition xvelocity yvelocity zvelocity g_base bounce) edit end_cond â™ - ht_list_test: List[â„] ☠= red_ht (cons (prep xposition yposition zposition xvelocity yvelocity zvelocity g_base bounce) nil) â™ - fun_list_test : List[℠⟶ (℠× ℠× â„)] ☠= red_funcs (cons (prep xposition yposition zposition xvelocity yvelocity zvelocity g_base bounce) nil) â™ - //ht_list: List[â„] ☠= red_ht full_list â™ - //fun_list : List[℠⟶ (℠× ℠× â„)] ☠= red_funcs full_list â™ + ht_list: List[â„] ☠= full_list map ([xele] red_ht xele) â™ + fun_list : List[℠⟶ (℠× ℠× â„)] ☠= full_list map ([vals] get_pos_fun (Ï€l (Ï€l vals)) (Ï€l (Ï€r (Ï€l vals))) (Ï€r (Ï€r (Ï€l vals))) (Ï€l (Ï€l (Ï€r vals))) (Ï€l (Ï€r (Ï€l (Ï€r vals)))) (Ï€r (Ï€r (Ï€l (Ï€r vals)))) (Ï€l (Ï€r (Ï€r vals)))) â™ meta ?MetaAnnotations?label "BouncingScroll" â™ meta ?MetaAnnotations?description s"Bouncing " â™ âš