Natural number to boolean array

Stream: new members

[Zahir Bingen]

Hello everyone,

I have defined a function that converts a boolean array to a natural number as follows:

def bool_arr_to_nat {n : ℕ} (v : array n bool) : ℕ :=
  let acc := 0 in
  v.foldl acc (λ b acc, cond b (2 * acc + 1) (2 * acc + 0))

Now I'm wondering, how can I define a function that takes a natural number, and returns an array n bool.
The issue I'm arising at is that the length returned by functions such as .to_array and nat.bits, are different in length.
How can I convert these lengths to n?

def nat_to_bool_array {n : ℕ} (num : ℕ) : (array n bool) :=
  if num = 0 then [ff].to_array else (nat.bits num).to_array

[Eric Wieser]

Note that your cond expression is docs#Nat.bit