Ros.Geometry_msgs.Quaternion

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 Quaternion := { _x : RoshaskFloat
                      ; _y : RoshaskFloat
                      ; _z : RoshaskFloat
                      ; _w : RoshaskFloat
                      }.

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