def impl_up

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64sqrt.bend:114

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X

114def impl_up(+fuel: Nat, +x: U32, +r: U32, +up: Bool) -> {X.up32(fuel, x, r, up) == up32g(fuel, x, r, up, 65535) : U32}:
115  match fuel up:
116    case 0n _:
117      {==}
118    case 1n+ +f False{}:
119      {==}
120    case 1n+ +f True{}:
121      impl_up(f, x, U32.add(r, 1), X.up_ok(x, U32.add(r, 1)))