@[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.

@[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.

@[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.