feat(library/init/data/hashable): add hashable nat instance

library/init/data/hashable.lean

@@ -10,14 +10,20 @@ universes u
 class hashable (α : Type u) :=
 (hash : α → usize)
 
+export hashable (hash)
+
 -- TODO: mark as builtin and opaque
 def mix_hash (u₁ u₂ : usize) : usize :=
 default usize
 
 -- TODO: mark as builtin
-def string.hash (s : string) : usize :=
+protected def string.hash (s : string) : usize :=
 default usize
 
 instance : hashable string := ⟨string.hash⟩
 
-export hashable (hash)
+-- TODO: add builtin
+protected def nat.hash (n : nat) : usize :=
+usize.of_nat n
+
+instance : hashable nat := ⟨nat.hash⟩

library/init/lean/name.lean

@@ -32,7 +32,7 @@ namespace name
 private def hash_aux : name → usize → usize
 | anonymous        r := r
 | (mk_string n s)  r := hash_aux n (mix_hash r (hash s))
-| (mk_numeral n k) r := hash_aux n (mix_hash r (usize.of_nat k))
+| (mk_numeral n k) r := hash_aux n (mix_hash r (hash k))
 
 -- TODO: mark as opaque and builtin, and add as builtin
 protected def hash (n : name) : usize :=