Struct Mmb

pub struct Mmb<'a> { /* private fields */ }

Implementations

impl<'a> Mmb<'a>

pub fn from(file: &'a [u8]) -> Option<Mmb<'a>>

Build a Mmb struct by parsing the file header

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

Return the slice containing the entire file

pub fn version(&self) -> u8

Return the version of the proof file format

pub fn num_sorts(&self) -> u8

Return the number of sorts in the sort table

pub fn num_terms(&self) -> u32

Return the number of terms in the term table

pub fn num_theorems(&self) -> u32

Return the number of theorems in the theorem table

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

Return the slice containing the sort table

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

Return the slice containing the term table

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

Return the slice containing the theorem table

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

Return the slice containing the proof section

pub fn index(&self) -> Option<&Index<'_>>

Return a reference to the optional index section

pub fn visit<V: Visitor<'a>>( &self, visitor: &mut V, ) -> Result<(), Err<ParseError<'_>>>

Trait Implementations

impl<'a> Debug for Mmb<'a>

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

Formats the value using the given formatter.