α : Type u_1
β : Type u_2
n : Nat
h : 0 < n
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) (List.replicate n AssocList.nil)) = 0
α : Type u_1
β : Type u_2
n : Nat
h : 0 < n
⊢ size (mk n) = 0
simp [Bucket.size_eq, Bucket.mk, mkArray]
α : Type u_1
β : Type u_2
n : Nat
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) (List.replicate n AssocList.nil)) = 0
α : Type u_1
β : Type u_2
n : Nat
h : 0 < n
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) (List.replicate n AssocList.nil)) = 0
clear h
no goals
α : Type u_1
β : Type u_2
n : Nat
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) (List.replicate n AssocList.nil)) = 0
induction n <;> simp [*]