Struct Names 

pub struct Names { /* private fields */ }

Implementations

impl Names

pub fn new() -> Names

pub fn intern(&mut self, node: NameNode) -> NameId

pub fn str(&mut self, prefix: NameId, s: &str) -> NameId

pub fn component(&self, sym: Symbol) -> &str

pub fn num(&mut self, prefix: NameId, n: u64) -> NameId

pub fn dotted(&mut self, s: &str) -> NameId

Interns a dotted name such as Nat.succ. Only for well-known names written in source.

pub fn node(&self, id: NameId) -> &NameNode

pub fn prefix(&self, id: NameId) -> NameId

pub fn is_prefix_of(&self, p: NameId, n: NameId) -> bool

true when p is a (non-strict) prefix of n.

pub fn replace_prefix(&mut self, n: NameId, old: NameId, new: NameId) -> NameId

Replaces prefix old of n by new (n unchanged when old is not a prefix).

pub fn append_index_after(&mut self, n: NameId, i: u64) -> NameId

Lean’s Name.appendIndexAfter: u ↦ u_1.

pub fn append(&mut self, a: NameId, b: NameId) -> NameId

Lean’s Name.append.

pub fn display(&self, id: NameId) -> String

pub fn len(&self) -> usize

pub fn is_empty(&self) -> bool

Trait Implementations

impl Clone for Names

fn clone(&self) -> Names

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Default for Names

fn default() -> Self

Returns the “default value” for a type.