Cacher is the code snippet organizer for pro developers

theorem stopping_if_exists state =
  let open Sensor_msgs in
  match state.incoming with None | Some (Clock _ ) -> true 
  | Some ( Sensor data ) ->
  (  data.laserScan_ranges <> []
  && List.exists under_threshold data.laserScan_ranges
  ) ==> (one_step state).mode = Turning
[@@apply lemma1 state]
[@@apply bridge
    (match state.incoming with Some (Sensor data) -> data.laserScan_range_max | _ -> 0)
    (match state.incoming with Some (Sensor data) -> data.laserScan_ranges | _ -> []) ]
[@@induct]