Struct Name 

pub struct Name(/* private fields */);

A hierarchical name.

Names identify constants, inductives, and other declarations. They form a tree: Nat.add.comm is Str(Str(Str(Anonymous, "Nat"), "add"), "comm").

Structural sharing (wave5 Stage F): Name is a newtype over a reference-counted cell holding its outermost component (NameKind), so cloning a whole name — e.g. the name held by every Const referencing a constant — is an O(1) refcount bump, not a deep copy of the component chain. The parent link inside NameKind is itself a Name, so a name shares its entire prefix with any longer name built on it: at Mathlib scale (millions of recurring names and prefixes) residency is proportional to the number of distinct names, not to how many times each is referenced.

Each name also stores a hash of its own structure, computed when it is built from its parent’s stored hash and its last component (see the kernel-private structural_hash module) — so an Expr that mentions a name (a Const, a binder, a projection) folds it into its own hash in O(1), without walking the component chain.

Equality is exactly structural: the same allocation is equal, different stored hashes are different (equal names always hash equal), and otherwise the components are compared. Hash writes the components as it always did (not the stored hash), so a HashMap<Name, _> behaves as before.

Match on the outermost component through Name::view: a match name.view() { NameView::Str(parent, s) => .. } reads like the former match name { Name::Str(parent, s) => .. }.

Implementations

impl Name

pub fn view(&self) -> NameView<'_>

Borrow this name’s outermost component for matching. O(1).

pub fn anonymous() -> Name

The anonymous (root) name.

pub fn mk_str(parent: Name, s: impl Into<String>) -> Name

Construct parent.s (string component). O(1) in the length of the name — shares parent and reads its stored hash.

pub fn mk_num(parent: Name, n: u64) -> Name

Construct parent.n (numeric component). O(1) — shares parent and reads its stored hash.

pub fn str(s: impl Into<String>) -> Self

Create a simple string name (no parent).

pub fn append_str(self, s: impl Into<String>) -> Self

Append a string component to this name.

pub fn append_num(self, n: u64) -> Self

Append a numeric component to this name.

pub fn is_anonymous(&self) -> bool

Check if this is the anonymous name.

pub fn from_str(s: &str) -> Self

Create a Name from a dot-separated string.

Name::from_str("Nat.add.comm") produces the same as Name::str("Nat").append_str("add").append_str("comm").

pub fn depth(&self) -> usize

Returns the depth (number of components) of this name.

Anonymous has depth 0, Name::str("Nat") has depth 1, Name::str("Nat").append_str("add") has depth 2.

pub fn last_str(&self) -> Option<&str>

Return the last string component of this name, if any.

For Nat.add, returns Some("add").

pub fn last_num(&self) -> Option<u64>

Return the last numeric component, if any.

pub fn root(&self) -> Option<&str>

Return the root (top-level) component as a string.

For Nat.add.comm, returns "Nat".

pub fn prefix(&self) -> Name

Return the parent name (prefix with last component removed).

pub fn has_prefix(&self, prefix: &Name) -> bool

Check whether this name has prefix as a (strict) prefix.

Nat.add.comm.has_prefix(Nat) is true.

pub fn components(&self) -> Vec<String>

Collect all components from root to leaf.

Returns a vector of (is_num, string_or_num) pairs.

pub fn from_components(comps: &[String]) -> Self

Reconstruct a Name from a list of string components.

Numeric strings are converted to Num components.

pub fn replace_last(self, new_last: impl Into<String>) -> Self

Replace the last string component with new_last.

If the name ends in a numeric component, appends new_last instead.

pub fn freshen(self, suffix: u64) -> Self

Produce a “fresh” version of this name by appending a suffix number.

Used to avoid name collisions during elaboration.

pub fn in_namespace(&self, ns: &Name) -> bool

Check whether this name is in the given namespace.

A name is in namespace ns if it has ns as a strict prefix.

pub fn with_suffix(self, suffix: impl Into<String>) -> Self

Append a suffix string to this name.

pub fn to_ident_string(&self) -> String

Convert to a string suitable for use as a Rust identifier.

Dots and special characters are replaced with underscores.

pub fn prepend(self, prefix: Name) -> Self

Return a new name with the given prefix prepended.

pub fn is_str_name(&self) -> bool

Check whether this name is a string name (last component is a string).

pub fn is_num_name(&self) -> bool

Check whether this name is a numeric name (last component is a number).

Trait Implementations

impl Clone for Name

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Name

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats as Name(<kind>) — the output of the derived implementation when Name wrapped the component kind directly. Code that hashes or orders terms by their Debug text depends on this spelling.

impl Default for Name

fn default() -> Self

The anonymous name.

impl Display for Name

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for Name

impl FromIterator<Name> for NameSet

fn from_iter<I: IntoIterator<Item = Name>>(iter: I) -> Self

Creates a value from an iterator.

impl Hash for Name

fn hash<H: Hasher>(&self, state: &mut H)

Writes the component chain, exactly as the derived implementation did when Name wrapped the component kind directly.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Ord for Name

fn cmp(&self, other: &Self) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

fn clamp_to<R>(self, range: R) -> Self

where Self: Sized, R: ClampBounds<Self>,

🔬This is a nightly-only experimental API. (clamp_to)

Restrict a value to a certain range.

impl PartialEq for Name

fn eq(&self, other: &Name) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl PartialOrd for Name

fn partial_cmp(&self, other: &Self) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.