mathlib documentation

core / init.meta.name

inductive name :

Type

anonymous : name
mk_string : string → name → name
mk_numeral : unsigned → name → name

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

auto_param α tac_name = α

@[simp]

theorem auto_param_eq (α : Sort u) (n : name) :

auto_param α n = α

@[protected, instance]

def name.inhabited :

Equations

name.inhabited = {default := name.anonymous}

def mk_str_name (n : name) (s : string) :

Equations

n <.> s = name.mk_string s n

def mk_num_name (n : name) (v : ℕ) :

Equations

mk_num_name n v = name.mk_numeral (unsigned.of_nat' v) n

def mk_simple_name (s : string) :

Equations

mk_simple_name s = name.anonymous <.> s

@[protected, instance]

def string_to_name :

has_coe string name

Equations

string_to_name = {coe := mk_simple_name}

def name.get_prefix :

Equations

(name.mk_numeral s p).get_prefix = p
(name.mk_string s p).get_prefix = p
name.anonymous.get_prefix = name.anonymous

def name.update_prefix :

name → name → name

Equations

(name.mk_numeral s p).update_prefix new_p = name.mk_numeral s new_p
(name.mk_string s p).update_prefix new_p = name.mk_string s new_p
name.anonymous.update_prefix new_p = name.anonymous

def name.to_string_with_sep (sep : string) :

name → string

Equations

name.to_string_with_sep sep (name.mk_numeral v (name.mk_numeral ᾰ ᾰ_1)) = name.to_string_with_sep sep (name.mk_numeral ᾰ ᾰ_1) ++ sep ++ repr v
name.to_string_with_sep sep (name.mk_numeral v (name.mk_string ᾰ ᾰ_1)) = name.to_string_with_sep sep (name.mk_string ᾰ ᾰ_1) ++ sep ++ repr v
name.to_string_with_sep sep (name.mk_numeral v name.anonymous) = repr v
name.to_string_with_sep sep (name.mk_string s (name.mk_numeral ᾰ ᾰ_1)) = name.to_string_with_sep sep (name.mk_numeral ᾰ ᾰ_1) ++ sep ++ s
name.to_string_with_sep sep (name.mk_string s (name.mk_string ᾰ ᾰ_1)) = name.to_string_with_sep sep (name.mk_string ᾰ ᾰ_1) ++ sep ++ s
name.to_string_with_sep sep (name.mk_string s name.anonymous) = s
name.to_string_with_sep sep name.anonymous = "[anonymous]"

def name.components (n : name) :

Equations

n.components = (name.components' n).reverse

@[protected]

def name.to_string :

name → string

Equations

name.to_string = name.to_string_with_sep "."

@[protected]

def name.repr (n : name) :

Equations

n.repr = "`" ++ n.to_string

@[protected, instance]

def name.has_to_string :

has_to_string name

Equations

name.has_to_string = {to_string := name.to_string}

@[protected, instance]

def name.has_repr :

Equations

name.has_repr = {repr := name.repr}

@[instance]

meta constant name.has_decidable_eq :

decidable_eq name

meta constant name.cmp :

name → name → ordering

meta constant name.lex_cmp :

name → name → ordering

meta constant name.append :

name → name → name

meta constant name.is_internal :

@[protected]

meta def name.lt (a b : name) :

Prop

@[protected, instance]

meta def name.lt.decidable_rel :

decidable_rel name.lt

@[protected, instance]

meta def name.has_lt :

@[protected, instance]

meta def name.has_append :

has_append name

meta constant name.append_after :

name → ℕ → name

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

meta def name.is_prefix_of :

name → name → bool

meta def name.is_suffix_of :

name → name → bool

meta def name.replace_prefix :

name → name → name → name