Enum ProofPositionSelector 

pub enum ProofPositionSelector {
    Default,
    Index {
        index: u32,
    },
    AfterText {
        text: String,
        occurrence: Option<u32>,
    },
    Entry,
}

Intent selector for one proof position inside a declaration.

Variants

Default

The first tactic state — the point after the first tactic has run.

Index

The index-th tactic state — after the index-th tactic has run.

Fields

index: u32

AfterText

The tactic whose source text exactly matches text.

Fields

text: String

occurrence: Option<u32>

Entry

The goal state before any tactic runs — the pristine entry goal. A proof attempt splices its candidate before the first tactic, so a from-scratch tactic block elaborates against this goal.

Trait Implementations

impl Clone for ProofPositionSelector

fn clone(&self) -> ProofPositionSelector

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofPositionSelector

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

Formats the value using the given formatter.

impl Default for ProofPositionSelector

fn default() -> ProofPositionSelector

Returns the “default value” for a type.

impl Eq for ProofPositionSelector

impl<'lean> IntoLean<'lean> for ProofPositionSelector

fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean>

Allocate (or scalar-box) a Lean representation of self and return the owned handle.

impl PartialEq for ProofPositionSelector

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for ProofPositionSelector