def add_value

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addv.bend:151

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F

151def add_value(+x: F.F64, +y: F.F64) -> SF.Add.value(x, y):
152  match x y:
153    case F.Bits{+xl, +xh} F.Bits{+yl, +yh}:
154      top_c(xl, xh, yl, yh, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), {==}, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), {==})