(module raw_buf_borrow_read (fn read_one (doc "Reads its borrow-mode RawBuf receiver via RawBuf.get once. get is a borrow-receiver op (kernel raw_buf: get : (borrow (RawBuf a)) Int -> a), so reading the receiver through a borrow must check clean — the receiver is read, not consumed.") (type (fn-type (params (borrow (con RawBuf (con Int)))) (ret (own (con Int))))) (params buf) (body (app RawBuf.get buf 0))) (fn count (doc "Reads its borrow-mode RawBuf receiver via RawBuf.size once. size is a borrow-receiver op (kernel raw_buf: size : (borrow (RawBuf a)) -> Int), so it must check clean for the same reason.") (type (fn-type (params (borrow (con RawBuf (con Int)))) (ret (own (con Int))))) (params buf) (body (app RawBuf.size buf))))