def init2
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend as Loopimport Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as T
28def init2(rest: List<&2,T.Out>, +x: T.Out) -> List<&2,T.Out>:
29 match rest:
30 case Nil{}: Nil{}
31 case Con{y,r}: Con{x,init2(r,y)}
Uses (2)
Used by (5)
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop:len_init2
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop:run2_split
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop:run_tree
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop:run_tree_go
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop:snoc2