Websocket.push: def of bend-kit-websocket@0.4.0.0
Import: import bend-kit-websocket@0.4.0.0/websocket.bend as Websocket
Lines 565-569 of bend-kit-websocket@0.4.0.0/websocket.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&start_line=565&end_line=569

import Base
import bend-kit-bytes@0.3.3.0/bytes.bend as Bytes

# The input with a read after it. Decoded octets are dropped first, so each octet is
# copied once for the frame it ends up in; when there are none, the read goes into the same buffer.
def push(c: Bytes.Cursor, read: Bytes.Bytes) -> Bytes.Cursor:
  Bytes.Cursor{Bytes.Bytes{+n, buf}, +pos, start, +end} = c
  push.when(Bool.and(U32.is_eq(pos, 0), U32.is_eq(end, n)), Bytes.Bytes{n, buf}, pos, end, read)

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=bend-kit-bytes@0.3.3.0/bytes.bend&name=Bytes
  https://jend.leeeet.dev/definition.txt?path=bend-kit-bytes@0.3.3.0/bytes.bend&name=Cursor
  https://jend.leeeet.dev/definition.txt?path=bend-kit-websocket@0.4.0.0/websocket.bend&name=push.when