word.bend checks
raw source on the hub · import 0xb13667d52aa56e002b4d09883d7fce3e/word.bend as MWord
word.bend: the vocabulary wordlib's laws are stated in.
1 import
import Base
Definitions
def b2n source · line 6 · raw
@b:Bool -> Nat
a bit as a Nat
def scale source · line 14 · raw
@k:Bool -> @p:Nat -> Nat
p if k, else 0n
def pow2 source · line 21 · raw
@n:Nat -> Nat
def maj source · line 29 · raw
@a:Bool -> @b:Bool -> @c:Bool -> Bool
majority of three bits: a full adder's carry out
def carry source · line 41 · raw
@n:Nat -> @a:Word(n) -> @b:Word(n) -> @c:Bool -> Bool
the carry out of Word.adc's add: the bit an n-bit sum overflows into
def top source · line 51 · raw
@n:Nat -> @c:Bool -> @w:Word(n) -> Bool
the bit Word.shl.put(n, c, w) shifts out: w's top bit, or c when n is 0
def lsb source · line 61 · raw
@n:Nat -> @w:Word(n) -> Bool
the lowest bit (False for the empty word)
def mulq source · line 73 · raw
@+n:Nat -> @m:Nat -> @a:Word(m) -> @+b:Word(n) -> @+acc:Word(n) -> Nat
how many times Word.mul.go's result wrapped past 2^n: each step adds the carry of acc + b (on a 1 bit) and, for every later bit of a, the top bit that shl pushed out of b