def sub_mag
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as F64import Base
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
184# (-1)^sa A + (-1)^sb B at a common scale x: equal magnitudes of opposite
185# signs cancel to +0 (round to nearest)
186def sub_mag(+sa: Bool, +a: Nat, +sb: Bool, +b: Nat, +x: Nat, c: Cmp) -> F.F64:
187 match c:
188 case GT{}:
189 round(sa, Nat.sub(a, b), x)
190 case LT{}:
191 round(sb, Nat.sub(b, a), x)
192 case EQ{}:
193 zero(False{})
Uses (7)
Used by (5)
- bend-collections-laws-math@1.0.0.0/spec/math/f64:add_mag
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf:caseEQ
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf:caseGT
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf:caseLT
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf:seq