Ros.Geometry_msgs.TwistWithCovariance

Extraction Language Haskell.
Require Import ROSCOQ.shim.Haskell.RoshaskNodeMonad.
Require Import ROSCOQ.shim.Haskell.RoshaskTopic.
Require Import ROSCOQ.shim.Haskell.RoshaskMsg.
Require Import ROSCOQ.shim.Haskell.RoshaskTypes.
Require Import String.
Require Import Data.Vector.Storable.
Require Import Ros.Geometry_msgs.Twist.

Record TwistWithCovariance := { _twist : Twist.Twist
                               ; _covariance : V.Vector P.Double
                               }.

Extract Inductive TwistWithCovariance ⇒ "Ros.Geometry_msgs.TwistWithCovariance.TwistWithCovariance" [ "Ros.Geometry_msgs.TwistWithCovariance.TwistWithCovariance" ].
Extract Constant _twist ⇒ "Ros.Geometry_msgs.TwistWithCovariance._twist" .
Extract Constant _covariance ⇒ "Ros.Geometry_msgs.TwistWithCovariance._covariance" .
Axiom subscribe : TopicName → Node (RTopic TwistWithCovariance ).
Extract Constant subscribe ⇒ "(Ros.Node.subscribe)".
Axiom publish : TopicName → RTopic TwistWithCovariance → Node unit.
Extract Constant publish ⇒ "(Ros.Node.advertise)".
Instance ROSMsgInstance : ROSMsgType TwistWithCovariance :=
Build_ROSMsgType _ subscribe publish.