~/bend-docscommunity

spec/lib/common.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as Common

1 import
import Base

Definitions

def pow2 source · line 7 · raw

@k:Nat -> Nat

2^k as a natural number.

def shift source · line 19 · raw

@k:Nat -> @+x:Nat -> Nat

Widths without powers: x * 2^k, n div 2^k and n mod 2^k by k doublings or halvings, and "n fits k bits". A literal 2^32 or 2^64 is beyond what the proof checker expands, so the fixed-width specifications (spec/math/generic, instances, w64) state widths through these; for a symbolic k they equal the pow2 forms (proofs/math/typed/width.bend).

def half source · line 27 · raw

@n:Nat -> Nat

n div 2 and n mod 2, structurally

def bit source · line 36 · raw

@n:Nat -> Nat

def high source · line 45 · raw

@k:Nat -> @+n:Nat -> Nat

def low source · line 52 · raw

@k:Nat -> @+n:Nat -> Nat

def fits source · line 60 · raw

@+k:Nat -> @+n:Nat -> Bool

n < 2^k

def length source · line 63 · raw

@-A:Data -> @xs:List<&2, A> -> Nat

def nth source · line 71 · raw

@-A:Data -> @xs:List<&2, A> -> @i:Nat -> Maybe<&2, A>

Element i, if any.

def update source · line 81 · raw

@-A:Data -> @xs:List<&2, A> -> @i:Nat -> @x:A -> List<&2, A>

Replace element i (no change when i is out of range).

def snoc source · line 90 · raw

@-A:Data -> @xs:List<&2, A> -> @x:A -> List<&2, A>

def last source · line 97 · raw

@-A:Data -> @xs:List<&2, A> -> Maybe<&2, A>

def init source · line 108 · raw

@-A:Data -> @xs:List<&2, A> -> List<&2, A>

def tail source · line 126 · raw

@-A:Data -> @xs:List<&2, A> -> List<&2, A>

def append source · line 133 · raw

@-A:Data -> @xs:List<&2, A> -> @ys:List<&2, A> -> List<&2, A>

def reverse source · line 140 · raw

@-A:Data -> @xs:List<&2, A> -> List<&2, A>

def replicate source · line 147 · raw

@-A:Data -> @n:Nat -> @+x:A -> List<&2, A>

def take source · line 154 · raw

@-A:Data -> @xs:List<&2, A> -> @n:Nat -> List<&2, A>

def drop source · line 163 · raw

@-A:Data -> @xs:List<&2, A> -> @n:Nat -> List<&2, A>

def memn source · line 173 · raw

@+s:Nat -> @xs:List<&2, Nat> -> Bool

membership of a natural number in a list of them