Ros.Geometry_msgs.Transform

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

Record Transform := { _translation : Vector3.Vector3
                     ; _rotation : Quaternion.Quaternion
                     }.

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