law when_true
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/proof.bend as Proofimport Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend as I
31law when_true:
32 for +ok: Bool
33 for +x: List<&2, U32>
34 for +h: {ok == True{} : Bool}
35 {I.when(ok, x) == Some{x} : Maybe<&2, List<&2, U32>>}
Uses (6)
Used by (4)
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/laws:chacha20.valid
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/laws:chacha20_block.valid
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/laws:hchacha20.valid
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/laws:xchacha20.valid