Changed the BouncingScroll to also return the hit time and functions

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 " ❙
     ❚