def push
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend as Blake3import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as T
161def push(s: Stack, c: T.CV) -> Stack:
162 match s:
163 case StkNil{}: SFull{c,StkNil{}}
164 case SEmpty{r}: SFull{c,r}
165 case SFull{d,r}: SEmpty{push(r,parent_cv(d,c))}
Uses (3)
Used by (13)
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop:run2
- bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3:pushed
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree:push_lift
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop:fuse_step2
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop:run2_run
- …