src/math/pow2.bend source

src/math/pow2.bend on the hub · documented module

import Base# 2^d by a TAIL recursion (an accumulator), so every def that calls it can# compile to a flat native loop. The structures' own `pow2` (the structural# `double(pow2(p))`, which the proofs unfold) is a non-tail recursion; the# native backend compiles a def that calls a non-tail recursion as a# segmented continuation instead of a flat loop, which made count, to_list,# the bitwise combinators and reserve several times slower than they need to# be. proofs/lib/pow2t.bend proves pow2t(d) == 2^d.def go(d: Nat, acc: Nat) -> Nat:  match d:    case 0n:      acc    case 1n+p:      go(p, Nat.double(acc))def pow2t(+d: Nat) -> Nat:  go(d, 1n)