~/bend-docscommunity

proofs/math/pow2/pow2.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/pow2/pow2.bend as Pow2

4 imports
import Base
import ../../lib/logic.bend as L
import ../../../spec/lib/common.bend as SC
import ../../../src/math/pow2.bend as P

Definitions

def go_double source · line 8 · raw

@+d:Nat -> @+acc:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/pow2.go(d, Nat.double(acc)) == Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/pow2.go(d, acc)) : Nat}

def same source · line 15 · raw

@+d:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/pow2.pow2t(d) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(d) : Nat}