n : ℕ
v : Bitvec n
⊢ Bitvec.toNat v = List.foldl (fun x y => flip addLsb y x) 0 (Vector.toList v)
n : ℕ
v : Bitvec n
⊢ Bitvec.toNat v = List.foldr (flip addLsb) 0 (List.reverse (Vector.toList v))
rw [List.foldr_reverse]
no goals
n : ℕ
v : Bitvec n
⊢ Bitvec.toNat v = List.foldl (fun x y => flip addLsb y x) 0 (Vector.toList v)
rfl