def checked_pick
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as Genericimport Base
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as N
63def checked_pick(~T: Data, ~of: Nat -> T, +n: Nat, ok: Bool) -> Result<&2, &2, N.NumError, T>:
64 match ok:
65 case True{}:
66 Done{of(n)}
67 case False{}:
68 Fail{N.Overflow{}}
Uses (4)
Used by (18)
- bend-collections-laws-math@1.0.0.0/spec/math/generic:checked
- bend-collections-laws-math@1.0.0.0/spec/math/generic:prefix_fin
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int:okfits
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int:okfits
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix32:cpow
- …