def hb2n

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqs.bend:20

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

20def hb2n(+c: Bool) -> {C.half(SF.b2n(c)) == 0n : Nat}:
21  match c:
22    case True{}:
23      {==}
24    case False{}:
25      {==}