~/jendhub

def p_append_empty_l

bend-osdev-bytes@0.1.1.0 · PROOF.bend:1318

import bend-osdev-bytes@0.1.1.0/PROOF.bend as PROOF
import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B

1318def p_append_empty_l(+o: B.Octets) -> {B.Octets.append(B.Octets.empty(), o) == o : B.Octets}:
1319  match o:
1320    case B.Octets{+ws}:
1321      %F_app(Nil{}, ws) : {B.Octets{_} == B.Octets{ws} : B.Octets}
1322      {==}

Uses (5)

Used by (1)