Struct NotationTable 

pub struct NotationTable { /* private fields */ }

The main notation/operator table.

Contains all registered notations and operators, supports scoped activation, and provides fast lookup by symbol.

Implementations

impl NotationTable

pub fn new() -> Self

Create an empty notation table.

pub fn register_notation(&mut self, entry: NotationEntry)

Register a notation entry.

pub fn register_operator(&mut self, entry: OperatorEntry)

Register an operator entry.

pub fn lookup_prefix(&self, symbol: &str) -> Option<&OperatorEntry>

Look up a prefix operator by symbol.

pub fn lookup_infix(&self, symbol: &str) -> Option<&OperatorEntry>

Look up an infix operator by symbol (either left- or right-associative).

pub fn lookup_postfix(&self, symbol: &str) -> Option<&OperatorEntry>

Look up a postfix operator by symbol.

pub fn lookup_operator(&self, symbol: &str) -> Option<&OperatorEntry>

Look up any operator by symbol regardless of fixity.

pub fn get_precedence(&self, symbol: &str) -> Option<u32>

Get the precedence of an operator by symbol.

pub fn get_entry(&self, index: usize) -> Option<&NotationEntry>

Get a notation entry by index.

pub fn notation_count(&self) -> usize

Get the number of registered notation entries.

pub fn operator_count(&self) -> usize

Get the number of registered operators.

pub fn open_scope(&mut self, scope: &str) -> Vec<&NotationEntry>

Open a scope, making its notations active.

Returns the notation entries that belong to that scope.

pub fn close_scope(&mut self, scope: &str)

Close a scope, deactivating its notations.

pub fn is_scope_active(&self, scope: &str) -> bool

Check whether a scope is currently active.

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

Get all currently active scopes.

pub fn active_notations(&self) -> Vec<&NotationEntry>

Get all currently active notations (global + active scopes).

pub fn find_by_name(&self, name: &str) -> Vec<&NotationEntry>

Find all notation entries matching a given name.

pub fn find_by_kind(&self, kind: &NotationKind) -> Vec<&NotationEntry>

Find all notation entries of a given kind.

pub fn find_operators_by_fixity(&self, fixity: &Fixity) -> Vec<&OperatorEntry>

Find all operators with a given fixity.

pub fn all_operator_symbols(&self) -> Vec<&str>

Get all operator symbols, sorted alphabetically.

pub fn compare_precedence(&self, a: &str, b: &str) -> Option<Ordering>

Compare the precedence of two symbols.

Returns Some(Ordering) if both symbols are registered, None otherwise.

pub fn builtin_operators() -> Self

Create a notation table pre-populated with standard Lean 4 operators.

Includes arithmetic, comparison, logical, arrow, and assignment operators with their standard precedences.

Trait Implementations

impl Clone for NotationTable

fn clone(&self) -> NotationTable

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for NotationTable

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

Formats the value using the given formatter.

impl Default for NotationTable

fn default() -> Self

Returns the “default value” for a type.