def snoc_ne

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

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/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend as S

147def snoc_ne(+xs: List<&2,T.Out>, +o: T.Out) -> {S.is_nil(SC.append(T.Out,xs,Con{o,Nil{}})) == False{} : Bool}:
148  match xs:
149    case Nil{}: {==}
150    case Con{+x,+r}: {==}