~/bend-docscommunity

proofs/math/pow2/pow2.bend checks

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

def same source · line 15 · raw

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