~/bend-docscommunity

proofs/math/pow2/pow2.bend checks

raw source on the hub · import bend-collections-laws-crypto@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 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/pow2.go(d, Nat.double(acc)) == Nat.double(0xa7e654f9780078ca65bf9e187da99d3e/src/math/pow2.go(d, acc)) : Nat}

def same source · line 15 · raw

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