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