ah. my bad: I had actually used
```
fun poll
{n: nat | n > 0}{l: addr}
( fds_pf: !array_v( pollfd_t, l, n) >> _ (* proof, that we have
access to address range (l,n), which contains initialized array of elements
of type pollfd_t *)
| fds: ptr l (* address *)
, nfds: size_t n (* range size *)
, timeout: int
): int = "ext#"
```
But misplaced refinement spec, while was writing email.
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAHjn2Kwnh%2Bis4K34MkBa%3DZLi-GQT8yy8F%3DFk0sRJRdrVkRxedA%40mail.gmail.com.
