def digit_value

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/phc.bend:167

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/words.bend as LW
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend as PH

167def digit_value(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 64n) == True{} : Bool}) -> {PH.value(PH.digit(x)) == Some{x} : Maybe<&2, U32>}:
168  %LW.rt(x) : {PH.value(PH.digit(_)) == Some{_} : Maybe<&2, U32>}
169  dv_n(U32.to_nat(x), h)