def okfits

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:812

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 NM

812def okfits(+x: Nat, +c: Bool) -> {G.ok(U32, G.fits(U32, Bool.not(c), of(x))) == SG.checked_pick(~U32, ~SG.u32_of, x, c) : Result<&2, &2, NM.NumError, U32>}:
813  match c:
814    case True{}:
815      {==}
816    case False{}:
817      {==}