Struct mmb_parser::index::Index

pub struct Index<'a> { /* fields omitted */ }

Index The index contains information about items in the proof file that are useful for printing and debugging purposes.

Implementations

impl<'a> Index<'a>

pub fn root_bst_ptr(&self) -> u64

Return a pointer to the root of the index binary search tree (BST)

pub fn sorts(&self) -> &[u8]

Return the slice of the data containing the pointers to the sort index entries

pub fn sort_pointer(&self, idx: usize) -> Option<u64>

Return the pointer to the sort index entry by index number

pub fn terms(&self) -> &[u8]

Return the slice of the data containing the pointers to the term index entries

pub fn term_pointer(&self, idx: usize) -> Option<u64>

Return the pointer to the sort index entry by index number

pub fn theorems(&self) -> &[u8]

Return the slice of the data containing the pointers to the theorem index entries

pub fn theorem_pointer(&self, idx: usize) -> Option<u64>

Return the pointer to the theorem index entry by index number

pub fn visit_sorts<V: Visitor>(&self, visitor: &mut V)

Visit all sorts in the index using the supplied visitor

pub fn visit_terms<V: Visitor>(&self, visitor: &mut V)

Visit all terms in the index using the supplied visitor

pub fn visit_theorems<V: Visitor>(&self, visitor: &mut V)

Visit all theorems in the index using the supplied visitor

pub fn sort(&self, idx: usize) -> Result<IndexEntry<'_>, Err<ParseError<'_>>>

Get the pointer to a sort index entry, and the entry data itself

pub fn term(&self, idx: usize) -> Result<IndexEntry<'_>, Err<ParseError<'_>>>

Get the pointer to a term index entry, and the entry data itself

pub fn theorem(&self, idx: usize) -> Result<IndexEntry<'_>, Err<ParseError<'_>>>

Get the pointer to a theorem index entry, and the entry data itself

Trait Implementations

impl<'a> Debug for Index<'a>

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

Formats the value using the given formatter.