1	import Base
2	import ../lib/common.bend as C
3	import ../../src/math/pow2.bend as P
4	
5	# Specification of src/math/pow2.bend: the tail-recursive power of two is
6	# the structural 2^d of spec/lib/common.bend.
7	#
8	#   function   clauses        proved in
9	#   pow2t      Pow2t.value    proofs/math/pow2/pow2.bend (same)
10	
11	def Pow2t.value(+d: Nat) -> Type:
12	  {P.pow2t(d) == C.pow2(d) : Nat}