def magc

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64cmp.bend:206

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
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

206# mag_cmp is the order of K on doubles that are not NaN
207def magc(+one: Nat, +h1: {one == 1n : Nat}, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +nx: {SF.is_nan(F.Bits{xl, xh}) == False{} : Bool}, +ny: {SF.is_nan(F.Bits{yl, yh}) == False{} : Bool}) -> {SF.mag_cmp(F.Bits{xl, xh}, F.Bits{yl, yh}) == Nat.cmp(Nat.add(SF.frac(F.Bits{xl, xh}), C.shift(52n, SF.efield(F.Bits{xl, xh}))), Nat.add(SF.frac(F.Bits{yl, yh}), C.shift(52n, SF.efield(F.Bits{yl, yh})))) : Cmp}:
208  magc_c(one, h1, xl, xh, yl, yh, nx, ny, SF.is_inf(F.Bits{xl, xh}), {==}, SF.is_inf(F.Bits{yl, yh}), {==})