mathlib3 documentation

core / init.meta.name

inductive name  :

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

Instances for name
@[reducible]
def auto_param (α : Sort u) (tac_name : name) :

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 = α
@[protected, instance]
Equations
def mk_str_name (n : name) (s : string) :
Equations
def mk_num_name (n : name) (v : ) :
Equations
@[protected, instance]
Equations
def name.components (n : name) :
Equations
@[protected]
def name.repr (n : name) :
Equations
@[protected, instance]
Equations
@[instance]

Both cmp and lex_cmp are total orders, but lex_cmp implements a lexicographical order.

meta constant name.cmp  :
meta constant name.append  :
meta constant name.is_internal  :
@[protected]
meta def name.lt (a b : name) :
Prop
Instances for name.lt
@[protected, instance]
@[protected, instance]
meta def name.has_lt  :
@[protected, instance]
meta constant name.append_after  :

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