def bit_u32
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend as Wideimport Base
51def bit_u32(b: Bool) -> U32:
52 match b:
53 case False{}:
54 0
55 case True{}:
56 1
Uses (2)
Used by (10)
- bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide:digit
- bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_shift:actual_candidate
- bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate_bound:million
- bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate_bound:native
- bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_invariant:digit
- …