Enum Tactic 

pub enum Tactic {
    Leaf(String),
    Sorry,
    Seq(Vec<Tactic>),
    First(Vec<Tactic>),
    Induction {
        target: String,
        arms: Vec<InductionArm>,
    },
}

A Lean tactic, modelled at the control level only.

Variants

Leaf(String)

One opaque tactic. May contain ; / <;> internally — not modelled.

Sorry

The sorry floor — rendered bare (sorry), never parenthesised.

Seq(Vec<Tactic>)

A by-block sequence: each step rendered on its own line, in order.

First(Vec<Tactic>)

first | b₁ | b₂ | … — the portfolio a minimizer collapses to one branch. Lean commits to the leftmost branch that closes, so the winner reported by the marker build is exactly the branch to keep.

Induction

induction <target> with + one arm per variant. Arm bodies are themselves tactics (they routinely contain their own Tactic::First).

Fields

target: String

arms: Vec<InductionArm>

Implementations

impl Tactic

pub fn raw(lines: Vec<String>) -> Tactic

Wrap already-rendered proof lines as an opaque sequence — the behavior-preserving bridge for proofs not yet structured into First nodes. raw(lines).render() == lines, so migrating a site to body: Tactic::raw(<old proof_lines>) is a no-op on the emitted Lean; only the portfolio sites that later become real Tactic::First trees gain anything for --minimize.

pub fn raw_dedented(lines: Vec<String>) -> Tactic

Like raw but first strips the lines’ common leading indent (keeping relative nesting). Use when wrapping already-rendered lines as a Tactic::First BRANCH: a branch is re-based under its | ( at render time, and when --minimize collapses the portfolio the branch is promoted flush with its new siblings — both want it authored at its own zero indent, not carrying the caller’s baked 2-space.

pub fn render(&self) -> Vec<String>

Render to the proof-body lines that follow := by (the caller supplies the theorem-level indent when it stitches these into the file). Produces valid Lean; formatting is normalised (it need not be byte-identical to the legacy string emit — the contract is that the proof still closes).

pub fn render_body(&self) -> Vec<String>

Render the proof body as it sits under a theorem’s := by — at the canonical 2-space indent.

raw-migrated bodies carry a baked-in leading indent in their leaf strings (the legacy emit indented every proof line by 2). Re-indenting that on top would double it, so this first strips the tree’s common leaf indent (preserving any deeper relative nesting) and then renders at indent 1. For a uniformly 2-space-baked body that is byte-identical to the legacy output; for a structured body (a real Tactic::First authored without baked indent) it lays the first/| keywords at the 2-space column the surrounding intro sits at — which Lean’s column-sensitive by block requires.

pub fn collapse_firsts( self, pick: &mut impl FnMut(&[Tactic]) -> Option<usize>, ) -> Tactic

The --minimize primitive: walk the tree, and for each Tactic::First ask pick which branch won (by the branch list); Some(i) collapses the portfolio to branch i (recursively minimized), None keeps it intact. pick is fed the Tactic::First nodes in pre-order, so a marker pass that numbered them in the same order can answer by index.

pub fn first_count(&self) -> usize

Count of Tactic::First nodes, in pre-order — the number of marker sites the instrument pass will emit and the winner pass will read back.

Trait Implementations

impl Clone for Tactic

fn clone(&self) -> Tactic

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Tactic

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

Formats the value using the given formatter.

impl Eq for Tactic

impl PartialEq for Tactic

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