Ros.Geometry_msgs.Accel

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.Geometry_msgs.Vector3.

Record Accel := { _linear : Vector3.Vector3
                 ; _angular : Vector3.Vector3
                 }.

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