def bit_c

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/f64bits.bend:329

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend as LW

329def bit_c(+c: Nat, +h2: {Nat.is_eq(C.half(c), 0n) == True{} : Bool}) -> {c == SF.b2n(Bool.not(Nat.is_eq(c, 0n))) : Nat}:
330  match c:
331    case 0n:
332      {==}
333    case 1n:
334      {==}
335    case 2n+ +q:
336      Empty.absurd({2n+q == SF.b2n(Bool.not(Nat.is_eq(2n+q, 0n))) : Nat}, LW.true_ne_false(Equal.sym(Bool, False{}, True{}, h2)))