Ros.Geometry_msgs.Point32

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.

Record Point32 := { _x : P.Float
                   ; _y : P.Float
                   ; _z : P.Float
                   }.

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