Ros.Geometry_msgs.Polygon

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 Data.Vector.Storable.
Require Import Ros.Geometry_msgs.Point32.

Record Polygon := { _points : V.Vector Point32.Point32
                   }.

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