def Iroot.done

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

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

213# a positive degree always has a root
214def Iroot.done(+n: Nat, +kp: Nat) -> Type:
215  Sigma<&1, &1, Nat, r => {M.iroot(n, 1n+kp) == Done{r} : Result<&2, &2, M.MathError, Nat>}>