def pushes_append

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/tree.bend:117

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend as K
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

117def pushes_append(+xs: List<&2,T.CV>, +s: K.Stack, +ys: List<&2,T.CV>) -> {push_all(s,SC.append(T.CV,xs,ys)) == push_all(push_all(s,xs),ys) : K.Stack}:
118  match xs:
119    case Nil{}: {==}
120    case Con{+c,+r}: pushes_append(r,K.push(s,c),ys)