def sq_val
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
150# the base squared, only while higher exponent bits remain
151def sq_val(~T: Data, ~op: N.Op<T> -> T, more: Bool, +b: T) -> T:
152 match more:
153 case False{}:
154 b
155 case True{}:
156 op(N.Mul{b, b})
Uses (2)
Used by (7)
- bend-collections-laws-math@1.0.0.0/src/math/generic:pow_go
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int:powsim
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int:powsim
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/float:pow_bin
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/float:sq_val_eq
- …