Ros.Geometry_msgs.Wrench

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 Wrench := { _force : Vector3.Vector3
                  ; _torque : Vector3.Vector3
                  }.

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