~/jendhub

def p_append_empty_r

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

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

1324def p_append_empty_r(+o: B.Octets) -> {B.Octets.append(o, B.Octets.empty()) == o : B.Octets}:
1325  match o:
1326    case B.Octets{+ws}:
1327      %F_app(ws, Nil{}) : {B.Octets{_} == B.Octets{ws} : B.Octets}
1328      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, List.append(&2, B.OctByte, ws, Nil{}), ws, app_nil8(ws))

Uses (9)

Used by (1)