Struct MineTask 

pub struct MineTask {

    pub task_id: String,
    pub project: String,
    pub file: LeanFile,
    pub declaration: Option<Declaration>,
    pub kind: MineKind,
    pub line: u32,
    pub column: u32,
    pub imports: Vec<String>,
    pub source_before: String,
    pub target_span: TargetSpan,
    pub source_after: String,
    pub diagnostic: Option<Diagnostic>,
    pub goal_state: Option<GoalState>,
    pub allowed_edit: AllowedEdit,
    pub instructions: String,
}

One mined, replayable proof task.

Fields

task_id: String

Stable identifier, shaped Module.decl:line (or Module:line when no declaration name is detected), with a :column suffix on collision.

project: String

Project the task was mined from.

file: LeanFile

Source file holding the span.

declaration: Option<Declaration>

Enclosing declaration, when one is detectable.

kind: MineKind

What this task targets.

line: u32

One-based line of the placeholder token or error site.

column: u32

Zero-based column of the placeholder token or error site.

imports: Vec<String>

Import lines in scope, in source order.

source_before: String

File text before the target span.

target_span: TargetSpan

The exact span to replace.

source_after: String

File text after the target span.

diagnostic: Option<Diagnostic>

Backing diagnostic for error tasks; absent for placeholder tasks.

goal_state: Option<GoalState>

Goal state when the backing diagnostic exposed one.

allowed_edit: AllowedEdit

The single span the replay step may edit.

instructions: String

Standing instruction for the agent.

Trait Implementations

impl Clone for MineTask

fn clone(&self) -> MineTask

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for MineTask

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for MineTask

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Eq for MineTask

impl PartialEq for MineTask

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

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 MineTask