fact: Fixpoint repair_hit_edge (g : edge) (evs : seq event) : seq event := match evs with | nil => nil | Bevent p gs :: evs' => match partition (fun g' => have_crossing g g') gs with | (nil, cg) => Bevent p gs :: repair_hit_edge g evs' | (bg :: _, cg) => match break_edges_at_crossing bg g with | (Some (e1, e2), _) => Bevent p (e1 :: cg) :: add_event (left_pt e2) e2 false evs' | (None, _) => nil end end end.
imports: Arith QArith List smooth_trajectories Reals