Struct TacticInfoNode 

pub struct TacticInfoNode {
    pub start_line: u32,
    pub start_column: u32,
    pub end_line: u32,
    pub end_column: u32,
    pub goals_before: Vec<String>,
    pub goals_after: Vec<String>,
}

One Lean.Elab.TacticInfo projection.

goals_before / goals_after are already pretty-printed by the Lean shim inside the elaboration’s MetaM context. Empty arrays mean the elaborator recorded the tactic without an enclosing goals list (rare). The strings carry no metavariable identity that the Rust side can reuse — they are diagnostic text only.

Fields

start_line: u32

1-based start line.

start_column: u32

1-based start column.

end_line: u32

1-based end line.

end_column: u32

1-based end column.

goals_before: Vec<String>

Goals as the user would see them before this tactic ran.

goals_after: Vec<String>

Goals as the user would see them after this tactic ran.

Trait Implementations

impl Clone for TacticInfoNode

fn clone(&self) -> TacticInfoNode

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TacticInfoNode

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

Formats the value using the given formatter.

impl PartialEq for TacticInfoNode

fn eq(&self, other: &TacticInfoNode) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<'lean> TryFromLean<'lean> for TacticInfoNode

fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self>

Decode obj into Self, returning a LeanError::Host with stage [HostStage::Conversion] if the object’s kind or payload is outside the type’s representable range.

impl Eq for TacticInfoNode

impl StructuralPartialEq for TacticInfoNode