def nd_head

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend as PH

1149def nd_head(+c: Char, +r: String, +h: {nd(SCon{c, r}) == True{} : Bool}) -> {PH.dollar(SCon{c, SNil{}}) == False{} : Bool}:
1150  +e = L.and_left(Bool.not(PH.dollar(SCon{c, SNil{}})), nd(r), h)
1151  L.not_true(PH.dollar(SCon{c, SNil{}}), e)