Generic.FPow.binary: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as Generic Lines 273-274 of bend-collections-laws-math@1.0.0.0/spec/math/generic.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/generic.bend&start_line=273&end_line=274 import Base import bend-collections-laws-math@1.0.0.0/src/math/num.bend as N import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G def FPow.binary(~T: Data, ~op: N.Op -> T, ~test: N.Test -> Bool, +x: T, +k: Nat) -> Type: {G.pow(~T, ~op, ~test, x, k) == Done{binpow(~T, ~op, 1n+k, k, x, op(N.One{}))} : Result<&2, &2, N.NumError, T>} Uses (8): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/generic.bend&name=binpow https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/generic.bend&name=pow https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/num.bend&name=NumError https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/num.bend&name=Op https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/num.bend&name=Test