def start_index
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as Argon2import Base
353def start_index(first: Bool) -> Nat:
354 match first:
355 case True{}:
356 2n
357 case False{}:
358 0n
Uses (2)
Used by (5)
- bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2:segment
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill:segment_len
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill:segment_eq
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill:start_index_le
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/index:start_index_eq