def imid
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as Genericimport Base
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as N
379# lo + (hi - lo) / 2, never above hi
380def imid(~T: Data, ~op: N.Op<T> -> T, +lo: T, +hi: T) -> T:
381 op(N.Add{lo, op(N.Half{op(N.Sub{hi, lo})})})
Uses (1)
Used by (8)
- bend-collections-laws-math@1.0.0.0/src/math/generic:search_go
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int:imid_v
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int:imid_v
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int:iroot_big
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int:srch
- …