ROSCOQ.shim.Haskell.RoshaskMsg

Require Import String.
Require Import ExtrHaskellString.
Require Import ROSCOQ.CoList.
Require Import RoshaskNodeMonad.
Require Import RoshaskTopic.


Class ROSMsgType (T:Type) :=
  {
   subscribe : TopicName → Node (RTopic T);
   publish : TopicName → RTopic T → Node unit
   
}.


Require ExtrHaskellZNum.
Require Import ZArith.
Axiom delayMsgsRoshask : ∀ {A:Type}, (A → Z) → (RTopic A) → (RTopic A).
Extract Constant delayMsgsRoshask ⇒ "Ros.ROSCoqUtil.delayMsgs".
Definition delayResolutionSecInv : positive := (1000000)%positive.