mathlib

9ed9e0f8 - feat(tactic/has_variable_names): add tactic for type-based naming (#4988)

feat(tactic/has_variable_names): add tactic for type-based naming (#4988) When we name hypotheses or variables, we often do so in a type-directed fashion: a hypothesis of type `ℕ` is called `n` or `m`; a hypothesis of type `list ℕ` is called `ns`; etc. This commits adds a tactic which looks up typical variable names for a given type. Typical variable names are registered by giving an instance of the new type class `has_variable_names`. We also give instances of this type class for many core types.