#ifndef __VHEX_TIMER_TYPES__
# define __VHEX_TIMER_TYPES__
/* force uint64_t */
#include <stdint.h>
/* timer ID */
typedef int tid_t;
#endif /* __VHEX_TIMER_TYPES__ */