def up32g

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

import Base

105def up32g(fuel: Nat, +x: U32, +r: U32, up: Bool, +m: U32) -> U32:
106  match fuel up:
107    case 0n _:
108      r
109    case 1n+f False{}:
110      r
111    case 1n+f True{}:
112      up32g(f, x, U32.add(r, 1), up_okg(x, U32.add(r, 1), m), m)