def from_nat_value

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/lemmas/proofs/word_value.bend:112

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

112def from_nat_value(n: Nat, +v: Nat, h: {Nat.is_lt(v, Nat.pow(2n, n)) == True{} : Bool}) -> {S.unsigned(n, S.from_nat(n, v)) == v : Nat}:
113  match n:
114    case 0n: below_one(v, h)
115    case 1n++p: from_nat_step(p, v, half_parts(v), h, q => hq => from_nat_value(p, q, hq))