def li.drop_append

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:205

import bend-osdev-cipher-modes@0.1.0.0/PROOF.bend as PROOF

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B

205def li.drop_append(+a: List<&2, U32>, +b: List<&2, U32>) -> {B.drop(B.len(a), B.append(a, b)) == b : List<&2, U32>}:
206  match a:
207    case Nil{}:
208      {==}
209    case Con{+h, +t}:
210      li.drop_append(t, b)

Uses (5)

Used by (2)