Ros.Geometry_msgs.Pose

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.Point.
Require Import Ros.Geometry_msgs.Quaternion.

Record Pose := { _position : Point.Point
                ; _orientation : Quaternion.Quaternion
                }.

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