def half
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as Commonimport Base
26# n div 2 and n mod 2, structurally
27def half(n: Nat) -> Nat:
28 match n:
29 case 0n:
30 0n
31 case 1n:
32 0n
33 case 2n+q:
34 1n+half(q)
Uses (1)
Used by (57)
- bend-collections-laws-crypto@1.0.0.0/spec/lib/common:high
- bend-collections-laws-crypto@1.0.0.0/spec/lib/common:low
- bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand:and_bits
- bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width:low_high
- bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/shrn:shrn_high
- …