mathlib3 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
```
source
@[class]
structure has_variable_names (α : Sort u) :
Type

Type class for associating a type α with typical variable names for elements of α. See tactic.typical_variable_names.

Instances of this typeclass
Instances of other typeclasses for has_variable_names
  • has_variable_names.has_sizeof_inst
source
meta def tactic.typical_variable_names (t : expr) :
tactic (list name)

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]
source
def has_variable_names.make_listlike_instance (α : Sort u) [has_variable_names α] {β : Sort v} :
has_variable_names β

@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
source
def has_variable_names.make_inheriting_instance (α : Sort u) [has_variable_names α] {β : Sort v} :
has_variable_names β

@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
source
@[protected, instance]
def d_array.has_variable_names {n : ℕ} {α : Type u_1} [has_variable_names α] :
has_variable_names (d_array n (λ (_x : fin n), α))
Equations
source
@[protected, instance]
def bool.has_variable_names  :
has_variable_names bool
Equations
source
@[protected, instance]
def char.has_variable_names  :
has_variable_names char
Equations
source
@[protected, instance]
def fin.has_variable_names {n : ℕ} :
has_variable_names (fin n)
Equations
source
@[protected, instance]
def int.has_variable_names  :
has_variable_names ℤ
Equations
source
@[protected, instance]
def list.has_variable_names {α : Type u_1} [has_variable_names α] :
has_variable_names (list α)
Equations
source
@[protected, instance]
def nat.has_variable_names  :
has_variable_names ℕ
Equations
source
@[protected, instance]
def Prop.has_variable_names  :
has_variable_names Prop
Equations
source
@[protected, instance]
def thunk.has_variable_names {α : Type u_1} [has_variable_names α] :
has_variable_names (thunk α)
Equations
source
@[protected, instance]
def prod.has_variable_names {α : Type u_1} {β : Type u_2} :
has_variable_names (α × β)
Equations
source
@[protected, instance]
def pprod.has_variable_names {α : Sort u_1} {β : Sort u_2} :
has_variable_names (pprod α β)
Equations
source
@[protected, instance]
def sigma.has_variable_names {α : Type u_1} {β : α → Type u_2} :
has_variable_names (sigma β)
Equations
source
@[protected, instance]
def psigma.has_variable_names {α : Sort u_1} {β : α → Sort u_2} :
has_variable_names (psigma β)
Equations
source
@[protected, instance]
def subtype.has_variable_names {α : Sort u_1} [has_variable_names α] {p : α → Prop} :
has_variable_names (subtype p)
Equations
source
@[protected, instance]
def option.has_variable_names {α : Type u_1} [has_variable_names α] :
has_variable_names (option α)
Equations
source
@[protected, instance]
def bin_tree.has_variable_names {α : Type u_1} :
has_variable_names (bin_tree α)
Equations
source
@[protected, instance]
def rbtree.has_variable_names {α : Type u_1} [has_variable_names α] {lt : α → α → Prop} :
has_variable_names (rbtree α lt)
Equations
source
@[protected, instance]
meta def native.rb_set.has_variable_names {α : Type u_1} [has_variable_names α] :
has_variable_names (native.rb_set α)
source
@[protected, instance]
def set.has_variable_names {α : Type u_1} [has_variable_names α] :
has_variable_names (set α)
Equations
source
@[protected, instance]
def string.has_variable_names  :
has_variable_names string
Equations
source
@[protected, instance]
def unsigned.has_variable_names  :
has_variable_names unsigned
Equations
source
@[protected, instance]
def pi.has_variable_names {α : Sort u_1} {β : α → Sort u_2} :
has_variable_names (Π (a : α), β a)
Equations
source
@[protected, instance]
def name.has_variable_names  :
has_variable_names name
Equations
source
@[protected, instance]
meta def tactic.has_variable_names {α : Type u_1} :
has_variable_names (tactic α)
source
@[protected, instance]
meta def expr.has_variable_names  :
has_variable_names expr
source
@[protected, instance]
meta def pexpr.has_variable_names  :
has_variable_names pexpr
source
@[protected, instance]
meta def level.has_variable_names  :
has_variable_names level
source
@[protected, instance]
def binder_info.has_variable_names  :
has_variable_names binder_info
Equations