spec/math/pow2.bend

bend-collections-laws-math@1.0.0.0 · 12 lines · 1 definition

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/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
11def Pow2t.value(+d: Nat) -> Type:
12  {P.pow2t(d) == C.pow2(d) : Nat}