Ros.Geometry_msgs.Inertia

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 Inertia := { _m : RoshaskFloat
                   ; _com : Vector3.Vector3
                   ; _ixx : RoshaskFloat
                   ; _ixy : RoshaskFloat
                   ; _ixz : RoshaskFloat
                   ; _iyy : RoshaskFloat
                   ; _iyz : RoshaskFloat
                   ; _izz : RoshaskFloat
                   }.

Extract Inductive Inertia ⇒ "Ros.Geometry_msgs.Inertia.Inertia" [ "Ros.Geometry_msgs.Inertia.Inertia" ].
Extract Constant _m ⇒ "Ros.Geometry_msgs.Inertia._m" .
Extract Constant _com ⇒ "Ros.Geometry_msgs.Inertia._com" .
Extract Constant _ixx ⇒ "Ros.Geometry_msgs.Inertia._ixx" .
Extract Constant _ixy ⇒ "Ros.Geometry_msgs.Inertia._ixy" .
Extract Constant _ixz ⇒ "Ros.Geometry_msgs.Inertia._ixz" .
Extract Constant _iyy ⇒ "Ros.Geometry_msgs.Inertia._iyy" .
Extract Constant _iyz ⇒ "Ros.Geometry_msgs.Inertia._iyz" .
Extract Constant _izz ⇒ "Ros.Geometry_msgs.Inertia._izz" .
Axiom subscribe : TopicName → Node (RTopic Inertia ).
Extract Constant subscribe ⇒ "(Ros.Node.subscribe)".
Axiom publish : TopicName → RTopic Inertia → Node unit.
Extract Constant publish ⇒ "(Ros.Node.advertise)".
Instance ROSMsgInstance : ROSMsgType Inertia :=
Build_ROSMsgType _ subscribe publish.