Ros.Geometry_msgs.Pose2D

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 Pose2D := { _x : RoshaskFloat
                  ; _y : RoshaskFloat
                  ; _theta : RoshaskFloat
                  }.

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