Struct ContextBundle 

pub struct ContextBundle {
    pub file: LeanFile,
    pub line: u32,
    pub total_lines: usize,
    pub declaration: Option<Declaration>,
    pub imports: Vec<String>,
    pub surrounding: SourceWindow,
    pub diagnostics: Vec<Diagnostic>,
    pub goal_state: Option<GoalState>,
    pub provenance: Option<Provenance>,
    pub suggested_prompt: String,
}

A compact context bundle around one line of a Lean file.

Fields

file: LeanFile

Source file the bundle describes.

line: u32

One-based target line, clamped into the file’s range.

total_lines: usize

Total number of source lines in the file.

declaration: Option<Declaration>

Enclosing declaration, when one is detectable.

imports: Vec<String>

Import lines found in the file, in source order.

surrounding: SourceWindow

Surrounding source window.

diagnostics: Vec<Diagnostic>

Diagnostics relevant to the target line, when a trace was run.

goal_state: Option<GoalState>

Goal state extracted from a relevant diagnostic, when present.

provenance: Option<Provenance>

Tooling provenance, when a trace was run.

suggested_prompt: String

Ready-to-paste prompt assembled from the fields above.

Implementations

impl ContextBundle

pub fn to_markdown(&self) -> String

Render the bundle as Markdown for human review or a chat paste.

Trait Implementations

impl Clone for ContextBundle

fn clone(&self) -> ContextBundle

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ContextBundle

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for ContextBundle

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Eq for ContextBundle

impl PartialEq for ContextBundle

fn eq(&self, other: &ContextBundle) -> 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 Serialize for ContextBundle

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for ContextBundle