def PowMod.value

bend-collections-laws-math@1.0.0.0 · spec/math/natural.bend:252

import Base
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M

252def PowMod.value(+b: Nat, +e: Nat, +mp: Nat) -> Type:
253  {M.pow_mod(b, e, 1n+mp) == Done{Nat.mod(Nat.pow(b, e), 1n+mp)} : Result<&2, &2, M.MathError, Nat>}