def fpow_binary

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/float.bend:147

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 N

147def fpow_binary(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~mo: NoMulOver(~T, ~test), +x: T, +k: Nat) -> SG.FPow.binary(~T, ~op, ~test, x, k):
148  %Equal.sym(Maybe<&2, T>, G.pow_go(~T, ~op, ~test, 1n+k, k, x, True{}, (op(N.One{}), True{})), Some{SG.binpow(~T, ~op, 1n+k, k, x, op(N.One{}))}, pow_bin(~T, ~op, ~test, ~mo, 1n+k, k, x, op(N.One{}))) : {G.ok(T, _) == Done{SG.binpow(~T, ~op, 1n+k, k, x, op(N.One{}))} : Result<&2, &2, N.NumError, T>}
149  {==}