@[inline]

def BitVec.ofFnLEAux {n : Nat} (m : Nat) (f : Fin n → Bool) : BitVec m

ofFnLEAux f returns the BitVec m whose ith bit is f i when i < m, little endian.

Equations

• BitVec.ofFnLEAux m f = Fin.foldr n (fun (i : Fin n) (v : BitVec m) => v.shiftConcat (f i)) 0

@[inline]

def BitVec.ofFnLE {n : Nat} (f : Fin n → Bool) : BitVec n

ofFnLE f returns the BitVec n whose ith bit is f i with little endian ordering.

Equations

• BitVec.ofFnLE f = BitVec.ofFnLEAux n f

@[inline]

def BitVec.ofFnBE {n : Nat} (f : Fin n → Bool) : BitVec n

ofFnBE f returns the BitVec n whose ith bit is f i with big endian ordering.

Equations

• BitVec.ofFnBE f = BitVec.ofFnLE fun (i : Fin n) => f i.rev