Enum TacticStep 

pub enum TacticStep {
    Intro(Vec<String>),
    Exact(Term),
    Apply(Term),
    Assumption,
    Exfalso,
    Constructor,
    Left,
    Right,
    Exists(Term),
    Have(String, Term),
    Rfl,
    Change(Term),
    Rewrite(Term, bool),
    Induction(String, Vec<Vec<String>>),
    Cases(String, Vec<Vec<String>>),
    Refine(Term),
    Subst(String),
    Injection(String, Vec<String>),
    Calc(Vec<(Term, Term)>),
    Cc,
    Decide,
    Simp(Vec<Term>),
}

One step of a tactic script (by intro A x; exact (refl A x)).

Variants

Intro(Vec<String>)

Exact(Term)

Apply(Term)

Assumption

Exfalso

Constructor

Left

Right

Exists(Term)

Have(String, Term)

Rfl

Change(Term)

Rewrite(Term, bool)

Induction(String, Vec<Vec<String>>)

Cases(String, Vec<Vec<String>>)

Refine(Term)

Subst(String)

Injection(String, Vec<String>)

Calc(Vec<(Term, Term)>)

calc [R₁ := p₁, R₂ := p₂, …]: each step an equation and its proof.

Cc

Decide

Simp(Vec<Term>)

simp [l₁, …]: rewrite by the lemmas (the context’s @[simp] set when none is named).

Trait Implementations

impl Clone for TacticStep

fn clone(&self) -> TacticStep

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TacticStep

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

Formats the value using the given formatter.

impl Display for TacticStep

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

Formats the value using the given formatter.

impl PartialEq for TacticStep

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