mathlib documentation

tactic.has_variable_names

A tactic for type-based naming of variables

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 module provides a tactic, tactic.typical_variable_names, which looks up typical variable names for a given type.

Typical variable names are registered by giving an instance of the type class has_variable_names. This file provides has_variable_names instances for many of the core Lean types. If you want to override these, you can declare a high-priority instance (perhaps localised) of has_variable_names. E.g. to change the names given to natural numbers:

def foo : has_variable_names  :=
⟨[`i, `j, `k]⟩

local attribute [instance, priority 1000] foo

typical_variable_names t obtains typical names for variables of type t. The returned list is guaranteed to be nonempty. Fails if there is no instance has_typical_variable_names t.

typical_variable_names `() = [`n, `m, `o]

@make_listlike_instance α _ β creates an instance has_variable_names β from an instance has_variable_names α. If α has associated names a, b, ..., the generated instance for β has names as, bs, ... This can be used to create instances for 'containers' such as lists or sets.

Equations

@make_inheriting_instance α _ β creates an instance has_variable_names β from an instance has_variable_names α. The generated instance contains the same variable names as that of α. This can be used to create instances for 'wrapper' types like option and subtype.

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]
def prod.has_variable_names {α : Type u_1} {β : Type u_2} :

Equations
@[instance]
def pprod.has_variable_names {α : Sort u_1} {β : Sort u_2} :

Equations
@[instance]
def sigma.has_variable_names {α : Type u_1} {β : α → Type u_2} :

Equations
@[instance]
def psigma.has_variable_names {α : Sort u_1} {β : α → Sort u_2} :

Equations
@[instance]

Equations
@[instance]
def rbtree.has_variable_names {α : Type u_1} [has_variable_names α] {lt : α → α → Prop} :

Equations
@[instance]

Equations
@[instance]
def pi.has_variable_names {α : Sort u_1} {β : α → Sort u_2} :
has_variable_names (Π (a : α), β a)

Equations
@[instance]

Equations
@[instance]
meta def tactic.has_variable_names {α : Type u_1} :

@[instance]

Equations