Skip to content

Instantly share code, notes, and snippets.

@KKostya

KKostya/lemma1.ml

Created July 26, 2018 06:58
Show Gist options
  • Save KKostya/690b864f2148fc45ca30d62f527ef2db to your computer and use it in GitHub Desktop.
Save KKostya/690b864f2148fc45ca30d62f527ef2db to your computer and use it in GitHub Desktop.
Download ZIP
Raw
lemma1.ml
let under_threshold x = x < 20000
lemma lemma1 state =
let open Sensor_msgs in
match state.incoming with None | Some (Clock _ ) -> true
| Some ( Sensor data ) ->
( data.laserScan_ranges <> []
&& under_threshold (get_min_range data.laserScan_range_max data.laserScan_ranges)
) ==> (one_step state).mode = Turning
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment