mathlib documentation

core / init.meta.name

inductive name  :
Type

Reflect a C++ name object. The VM replaces it with the C++ implementation.

def auto_param (α : Sort u) (tac_name : name) :
Sort u

Gadget for automatic parameter support. This is similar to the opt_param gadget, but it uses the tactic declaration names tac_name to synthesize the argument. Like opt_param, this gadget only affects elaboration. For example, the tactic will not be invoked during type class resolution.

Equations
@[simp]
theorem auto_param_eq (α : Sort u) (n : name) :
auto_param α n = α
def mk_str_name (n : name) (s : string) :
Equations
def mk_num_name (n : name) (v : ) :
Equations
def name.components (n : name) :
Equations
def name.repr (n : name) :
Equations
@[instance]
Equations
@[instance]
meta constant name.cmp  :
meta constant name.lex_cmp  :
meta constant name.append  :
namenamename
meta constant name.is_internal  :
meta def name.lt (a b : name) :
Prop
@[instance]
meta def name.has_lt  :
@[instance]
meta constant name.append_after  :
namename

name.append_after n i return a name of the form n_i

meta def name.is_prefix_of  :
namenamebool
meta def name.is_suffix_of  :
namenamebool
meta def name.replace_prefix  :
namenamenamename