F64cmp.magc: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as F64cmp
Lines 206-208 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend&start_line=206&end_line=208

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

# mag_cmp is the order of K on doubles that are not NaN
def 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}:
  magc_c(one, h1, xl, xh, yl, yh, nx, ny, SF.is_inf(F.Bits{xl, xh}), {==}, SF.is_inf(F.Bits{yl, yh}), {==})

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend&name=magc_c
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=efield
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=frac
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=is_inf
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=is_nan
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=mag_cmp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64