Struct move_model::ast::SpecBlockInfo

pub struct SpecBlockInfo {
    pub loc: Loc,
    pub target: SpecBlockTarget,
    pub member_locs: Vec<Loc>,
}

Information about a specification block in the source. This is used for documentation generation. In the object model, the original locations and documentation of spec blocks is reduced to conditions on a Spec, with expansion of schemas. This data structure allows us to discover the original spec blocks and their content.

Fields

loc: Loc

The location of the entire spec block.

target: SpecBlockTarget

The target of the spec block.

member_locs: Vec<Loc>

The locations of all members of the spec block.

Trait Implementations

impl Clone for SpecBlockInfo

fn clone(&self) -> SpecBlockInfo

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for SpecBlockInfo

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

Formats the value using the given formatter.