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 unameSort 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
Instances
@[simp]
theorem auto_param_eq (α : Sort u) (n : name) :
auto_param α n = α

def mk_str_name  :
namestringname

Equations

Equations
def name.repr  :

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  :
namename → 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