def dec_rt

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

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

1331# A decimal number followed by a non-digit is read back.
1332def dec_rt(+n: Nat, +c: Char, +Y: String, +hc: {PH.starts_digit(SCon{c, Y}) == False{} : Bool}) -> {PH.read(String.append(PH.decimal(n), SCon{c, Y})) == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}:
1333  +s = String.append(PH.dec_go(1n+n, n, SNil{}, Nat.is_lt(n, 10n)), SCon{c, Y})
1334  %Equal.sym(Bool, PH.starts_digit(s), True{}, sd_dec(1n+n, n, SNil{}, SCon{c, Y}, Nat.is_lt(n, 10n), {==}, N.lt_succ(n))) : {PH.read_check(s, _) == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}
1335  %Equal.sym(PH.Got, PH.read_go(s, 0n, True{}), PH.read_go(SCon{c, Y}, n, PH.starts_digit(SCon{c, Y})), dec_go_rt(1n+n, n, SNil{}, SCon{c, Y}, Nat.is_lt(n, 10n), {==}, N.lt_succ(n))) : {Some{_} == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}
1336  %Equal.sym(Bool, PH.starts_digit(SCon{c, Y}), False{}, hc) : {Some{PH.read_go(SCon{c, Y}, n, _)} == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}
1337  got_nd(n, c, Y)