def up64g

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64isq.bend:54

import Base
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

54def up64g(fuel: Nat, +n: WU.U64, +r: U32, up: Bool, +m: U32) -> U32:
55  match fuel up:
56    case 0n _:
57      r
58    case 1n+f False{}:
59      r
60    case 1n+f True{}:
61      up64g(f, n, U32.add(r, 1), up64_okg(n, U32.add(r, 1), m), m)