def ilog_top

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:710

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

710def ilog_top(+K: Nat, +hK: {K == 64n : Nat}, +n: WU.U64, +b: WU.U64, +bad: Bool, +hN: {Bool.or(Nat.is_eq(v(n), 0n), Nat.is_lt(v(b), 2n)) == bad : Bool}) -> {G.ilog_ok(~WU.U64, ~I.u64_op, ~I.u64_is, n, b, bad) == SG.lift_nat(M.ilog_ok(v(n), v(b), bad)) : Result<&2, &2, NM.NumError, Nat>}:
711  match bad:
712    case True{}:
713      {==}
714    case False{}:
715      ilog_fin(K, hK, n, b, v(b), {==}, or_false_r(Nat.is_eq(v(n), 0n), Nat.is_lt(v(b), 2n), hN))