def bb2n

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

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

27def bb2n(+c: Bool) -> {C.bit(SF.b2n(c)) == SF.b2n(c) : Nat}:
28  match c:
29    case True{}:
30      {==}
31    case False{}:
32      {==}