spec/math/pow2.bend source

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

import Baseimport ../lib/common.bend as Cimport ../../src/math/pow2.bend as P# Specification of src/math/pow2.bend: the tail-recursive power of two is# the structural 2^d of spec/lib/common.bend.##   function   clauses        proved in#   pow2t      Pow2t.value    proofs/math/pow2/pow2.bend (same)def Pow2t.value(+d: Nat) -> Type:  {P.pow2t(d) == C.pow2(d) : Nat}