def bz

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addc.bend:38

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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

38# a zero pattern with sign s
39def bz(+s: Bool) -> {FR.bits(s, 0n) == SF.zero(s) : F.F64}:
40  Equal.trans(F.F64, F.Bits{0, U32.from_nat(C.shift(31n, SF.b2n(s)))}, F.Bits{0, U32.from_nat(C.shift(31n, SF.pick(Nat, s, 1n, 0n)))}, SF.zero(s), Equal.cong(Nat, F.F64, z => F.Bits{0, U32.from_nat(C.shift(31n, z))}, SF.b2n(s), SF.pick(Nat, s, 1n, 0n), Equal.sym(Nat, SF.pick(Nat, s, 1n, 0n), SF.b2n(s), FR.pb(s, 1n, {==}))), bz0(1n, {==}, s, 2147483648, {==}))