Struct Name 

pub struct Name { /* private fields */ }

A hierarchical name — Lean’s Name, which is a LIST of components and not a string with dots.

The distinction is not cosmetic. To resolve a short name against an enclosing namespace at all you must be able to walk the PREFIXES of the current namespace, and to store the answer you must be able to re-compose one flat absolute key. A String with dots in it can do the second and not the first.

A component is whatever scan_name accepts — ONE grammar for both doors, so every name the declaration door takes is a name a term can spell. A «guillemet name» is ONE component even when it contains a ., which is how a name with a dot in it stays writable.

Implementations

impl Name

pub fn scan(text: &str) -> Option<(Name, usize)>

Read a name off the FRONT of text, returning it with the bytes consumed. Components are separated by . with no surrounding space — Outer.Inner.value is three components, and Outer. Inner is one component followed by a sentence terminator.

pub fn parse(text: &str) -> Option<Name>

Read a name that is the WHOLE of text.

pub fn from_parts(parts: Vec<String>) -> Option<Name>

A name from components already in hand. None for the empty list — there is no such name.

pub fn key(&self) -> String

The flat absolute key the kernel context is indexed by.

pub fn parts(&self) -> &[String]

The components, outermost first.

pub fn short(&self) -> &str

The final component — the short name, with every namespace stripped.

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

Everything but the final component: the namespace a DECLARATION name itself names. For Foo.Bar.baz that is Foo.Bar, and Lean elaborates such a declaration with Foo.Bar current — which is where a short name inside it finds its siblings.

pub fn key_reads_back(&self) -> bool

Does this name’s flat key read back as this same name?

The kernel Context is keyed by a flat String, so a name is only HOLDABLE if its key identifies it. «a.b» is ONE component and keys at a.b, which reads back as the TWO-component a.b — two different names, one key, and whichever is declared second answers to the other’s spelling with nothing reported. That is this lane’s own defect class (a short name quietly denoting a constant nobody wrote) arriving through the guillemet escape instead of through an open.

A key that reads back as NOTHING AT ALL (a name with spaces, weird?!name) is holdable: no term-level spelling produces that string either, so there is nothing for it to collide with, and the quoted form stays the escape it was built to be.

pub fn is_spelled_by(&self, written: &str) -> bool

Can the TERM door spell this name, written exactly as written?

★ THE INVARIANT, CHECKED RATHER THAN RESTATED. “Every name the declaration door accepts, a term can spell” is the rule this whole grammar exists for, and scan_name gives both doors one COMPONENT grammar — but the term door joins components with its own dot-postfix rule and reserves its own keywords, so two doors that agree about components can still disagree about whole names. Definition end : Nat := Zero. and Definition Outer.«a b» : Nat := Zero. both scanned clean and both produced a global no Check could ever name: write-only names, by a route the component grammar cannot see.

So rather than restate the term door’s rule here — two grammars again, one step removed — the declaration door hands the spelling to the term door and requires this same name back. The check reads the grammar it is checking against, so it cannot drift from it.

The surface is deliberately EMPTY: a name must be spellable with no notation in force, or it is a name whose readability depends on a macro that a later End can take away.

pub fn is_root_escaped(&self) -> bool

Is this name spelled with the _root_ escape?

pub fn after_prefix(&self, prefix: &Name) -> Option<Vec<String>>

The components of self that follow prefix, or None when prefix is not one.

Lean’s Name.isPrefixOf (Lean/Data/Name.lean:46-49) plus the replacePrefix that always follows it: resolveOpenDecls (Lean/ResolveName.lean:146-151) resolves an explicit open Foo (x) for x.y by testing that x is a PREFIX of x.y and swapping it for Foo.x. An equal name gives the EMPTY remainder, which is that rule’s other half (openedId == id, line 144) falling out of the same test.

Trait Implementations

impl Clone for Name

fn clone(&self) -> Name

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<(), Error>

Formats the value using the given formatter.

impl Display for Name

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

Formats the value using the given formatter.

impl Hash for Name

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

where __H: Hasher,

Feeds this value into the given Hasher.

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: &Name) -> 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.

impl PartialEq for Name

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl PartialOrd for Name

fn partial_cmp(&self, other: &Name) -> 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.

impl Eq for Name

impl StructuralPartialEq for Name