Generic.Pow.checked: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/spec/math/generic.bend as Generic Lines 211-212 of bend-collections-laws-crypto@1.0.0.0/spec/math/generic.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/generic.bend&start_line=211&end_line=212 import Base import bend-collections-laws-crypto@1.0.0.0/src/math/num.bend as N import bend-collections-laws-crypto@1.0.0.0/src/math/generic.bend as G def Pow.checked(~T: Data, ~op: N.Op -> T, ~test: N.Test -> Bool, ~val: T -> Nat, ~of: Nat -> T, +w: Nat, +x: T, +k: Nat) -> Type: {G.pow(~T, ~op, ~test, x, k) == checked(~T, ~of, w, Nat.pow(val(x), k)) : Result<&2, &2, N.NumError, T>} Uses (9): 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=Nat.pow https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/generic.bend&name=checked https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/generic.bend&name=pow https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/num.bend&name=NumError https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/num.bend&name=Op https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/num.bend&name=Test