Phc.digit_value: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend as Phc
Lines 167-169 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&start_line=167&end_line=169

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

def 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>}:
  %LW.rt(x) : {PH.value(PH.digit(_)) == Some{_} : Maybe<&2, U32>}
  dv_n(U32.to_nat(x), h)

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&name=dv_n
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/words.bend&name=rt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=digit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=value