Primitive recursiveness of binary-digit reconstruction

Main results

• Primrec.list_foldr_nat_bit: folding Nat.bit over a binary string is primitive recursive.

theorem Primrec.list_foldr_nat_bit : Primrec fun (l : List Bool) => List.foldr Nat.bit 0 l

Folding Nat.bit over a binary string, which inverts Nat.bits (Nat.foldr_bit_bits), is primitive recursive.