Struct StatementRef

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

A reference to a statement which knows its address and can be used to fetch statement information.

Implementations

impl StatementRef<'_>

pub fn token_iter<'a, 'b>( &'a self, names: &'a mut NameReader<'b>, ) -> StmtTokenIter<'a, 'b>

Returns a new iterator over tokens of a math expression. names caches the result of any name lookups performed.

impl<'a> StatementRef<'a>

pub const fn index(self) -> StatementIndex

Fetch the segment-local index of this statement.

pub const fn segment(self) -> SegmentRef<'a>

Back up from a statement reference to a segment reference.

pub const fn statement_type(self) -> StatementType

Gets the type of this statement. May be a pseudo-type.

pub const fn is_assertion(self) -> bool

Returns true if this statement is an Axiom ($a) or Provable ($p) statement.

pub const fn address(self) -> StatementAddress

Obtain a globally-meaningful address for this statement.

pub const fn scope_range(self) -> GlobalRange

Constructs a range from this statement to the end of the database or innermost enclosing scope construct.

This is the end range of a hypothesis or variable defined in this statement.

pub const fn in_group(self) -> bool

True if there is a ${ $} group wrapping this statement.

pub const fn label_span(&self) -> Span

Obtain the span corresponding to the statment label.

pub fn label(&self) -> &'a [u8]

Obtain the statment label.

This will be non-null iff the type requires a label; missing labels for types which use them cause an immediate rewrite to Invalid.

pub fn math_iter(&self) -> TokenIter<'a>

An iterator for the symbols in a statement’s math string.

pub const fn span_full(&self) -> Span

The textual span of this statement within the segment’s buffer.

Does not include trailing white space or surrounding comments; will include leading white space, so a concatenation of spans for all statements will reconstruct the segment source.

pub const fn span(&self) -> Span

The textual span of this statement within the segment’s buffer.

Does not include surrounding white space or comments, unlike span_full().

pub const fn math_len(&self) -> TokenIndex

Count of symbols in this statement’s math string.

pub const fn proof_len(&self) -> TokenIndex

Count of tokens in this statement’s proof string.

pub fn math_span(&self, ix: TokenIndex) -> Span

Given an index into this statement’s math string, find a textual span into the segment buffer.

pub fn proof_span(&self, ix: TokenIndex) -> Span

Given an index into this statement’s proof string, find a textual span into the segment buffer.

pub fn proof_spans(&self) -> &'a [Span]

Get the list of spans of tokens in the proof.

pub fn use_iter(&self) -> UseIter<'a>

Returns an iterator over the statements referenced in the proof.

pub fn math_at(&self, ix: TokenIndex) -> TokenRef<'a>

Given an index into this statement’s math string, get a reference to the math token.

pub fn proof_slice_at(&self, ix: TokenIndex) -> TokenPtr<'a>

Obtains textual proof data by token index.

pub fn associated_comment(&self) -> Option<StatementRef<'a>>

Get the “documentation” comment immediately preceding a $a $p statement, if it exists.

pub const fn comment_contents(&self) -> Span

The contents of a comment statement, excluding the $( and $) delimiters.

pub fn comment_parser(&self) -> CommentParser<'a>

Get an iterator over the markup items in this comment.

pub fn discouragements(&self) -> Discouragements

Parse the associated commment to get the discouragements (Proof modification / new usage discouraged) for this theorem.

pub fn parentheticals(&self) -> ParentheticalIter<'a>

Return an iterator over the parentheticals (like (Contributed by ...)) in this comment statement.

pub fn as_heading_comment(&self) -> Option<HeadingComment>

Returns a HeadingComment object for a heading comment (if it is actually a heading).

Trait Implementations

impl<'a> Clone for StatementRef<'a>

fn clone(&self) -> StatementRef<'a>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'a> Debug for StatementRef<'a>

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

Formats the value using the given formatter.

impl<'a> Copy for StatementRef<'a>