ControlCruise
Imports
import Control;
open Control;
import Math;
Types
Constructors
For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.
Functions
def speed (s : ControlCruise) : Float
def integral (s : ControlCruise) : Float
def step (s : ControlCruise) (command : Float) : ControlCruise
def invalid (s : ControlCruise) : Bool
def pi (kp : Float) (ki : Float) (error : Float) (integral : Float) : Float
def reference (error : Float) (integral : Float) : Float
def coast (error : Float) (integral : Float) : Float
def advance (policy : (error : Float) → (integral : Float) → Float) (s : ControlCruise) : ControlCruise
def cost (policy : (error : Float) → (integral : Float) → Float) (s : ControlCruise) : Float
def episode (horizon : Int | horizon ≥ 0 && horizon ≤ 500) (policy : (error : Float) → (integral : Float) → Float) (initial : ControlCruise) : Control
def training (policy : (error : Float) → (integral : Float) → Float) : Float
def held_out (policy : (error : Float) → (integral : Float) → Float) : Float