Ros.Geometry_msgs.TwistWithCovarianceStamped


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 Ros.Internal.Msg.HeaderSupport.
Require Import Ros.Geometry_msgs.TwistWithCovariance.
Require Import Ros.Std_msgs.Header.

Record TwistWithCovarianceStamped := { _header : Header.Header
                                      ; _twist : TwistWithCovariance.TwistWithCovariance
                                      }.

Extract Inductive TwistWithCovarianceStamped ⇒ "Ros.Geometry_msgs.TwistWithCovarianceStamped.TwistWithCovarianceStamped" [ "Ros.Geometry_msgs.TwistWithCovarianceStamped.TwistWithCovarianceStamped" ].
Extract Constant _header ⇒ "Ros.Geometry_msgs.TwistWithCovarianceStamped._header" .
Extract Constant _twist ⇒ "Ros.Geometry_msgs.TwistWithCovarianceStamped._twist" .
Axiom subscribe : TopicNameNode (RTopic TwistWithCovarianceStamped ).
Extract Constant subscribe ⇒ "(Ros.Node.subscribe)".
Axiom publish : TopicNameRTopic TwistWithCovarianceStampedNode unit.
Extract Constant publish ⇒ "(Ros.Node.advertise)".
Instance ROSMsgInstance : ROSMsgType TwistWithCovarianceStamped :=
Build_ROSMsgType _ subscribe publish.