def okfits

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:813

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
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

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