Enum TacticExpr 

pub enum TacticExpr {
    Basic(String),
    WithArgs(String, Vec<String>),
    Seq(Box<TacticExpr>, Box<TacticExpr>),
    Alt(Box<TacticExpr>, Box<TacticExpr>),
    AllGoals(Box<TacticExpr>, Box<TacticExpr>),
    Repeat(Box<TacticExpr>),
    Try(Box<TacticExpr>),
    First(Vec<TacticExpr>),
    Focus(usize, Box<TacticExpr>),
    All(Box<TacticExpr>),
    Any(Box<TacticExpr>),
    Block(Vec<TacticExpr>),
    Intro(Vec<String>),
    Apply(String),
    Exact(String),
    Rewrite(Vec<RewriteRule>),
    Simp(SimpArgs),
    Cases(String, Vec<CaseArm>),
    Induction(String, Vec<CaseArm>),
    Have(String, Option<String>, Box<TacticExpr>),
    Let(String, String),
    Show(String),
    Suffices(String, Box<TacticExpr>),
    Calc(Vec<CalcStep>),
    Conv(ConvSide, Box<TacticExpr>),
    Omega,
    Ring,
    Decide,
    NormNum,
    Constructor,
    Left,
    Right,
    Existsi(String),
    Clear(Vec<String>),
    Revert(Vec<String>),
    Subst(String),
    Contradiction,
    Exfalso,
    ByContra(Option<String>),
    Assumption,
    Trivial,
    Rfl,
    Intros(Vec<String>),
    Generalize(String, String),
    InductionPat(String, String),
    Obtain(String, Box<TacticExpr>),
    Rcases(String, Vec<String>),
    Tauto,
    AcRfl,
    Custom(CustomTactic),
    Located(Box<TacticExpr>, TacticLocation),
}

A parsed tactic expression.

Variants

Basic(String)

Basic tactic by name

WithArgs(String, Vec<String>)

Tactic with arguments

Seq(Box<TacticExpr>, Box<TacticExpr>)

Sequence of tactics (t1 ; t2)

Alt(Box<TacticExpr>, Box<TacticExpr>)

Alternative tactics (t1 <|> t2)

AllGoals(Box<TacticExpr>, Box<TacticExpr>)

All goals combinator (t <;> t’)

Repeat(Box<TacticExpr>)

Repeat tactic

Try(Box<TacticExpr>)

Try tactic (don’t fail if it fails)

First(Vec<TacticExpr>)

First successful alternative

Focus(usize, Box<TacticExpr>)

Focus on specific goal

All(Box<TacticExpr>)

All goals

Any(Box<TacticExpr>)

Any goal

Block(Vec<TacticExpr>)

Block of tactics: { t1; t2; ... }

Intro(Vec<String>)

Introduce hypotheses: intro x y z

Apply(String)

Apply a lemma: apply lem

Exact(String)

Provide an exact proof term: exact e

Rewrite(Vec<RewriteRule>)

Rewrite: rewrite [lem1, <-lem2]

Simp(SimpArgs)

Simplification: simp, simp only [lem1], simp [*]

Cases(String, Vec<CaseArm>)

Case analysis: cases x with | c1 => t1 | c2 => t2

Induction(String, Vec<CaseArm>)

Induction: induction x with | c => t

Have(String, Option<String>, Box<TacticExpr>)

Local hypothesis: have h : T := by t

Let(String, String)

Local definition: let x := e

Show(String)

Show goal form: show T

Suffices(String, Box<TacticExpr>)

Suffices: suffices h : T by t

Calc(Vec<CalcStep>)

Calculational proof

Conv(ConvSide, Box<TacticExpr>)

Conversion mode: conv_lhs => t or conv_rhs => t

Omega

omega decision procedure

Ring

Ring decision procedure

Decide

Decide (boolean decidability)

NormNum

Normalize numerals

Constructor

Apply constructor

Left

Choose left disjunct

Right

Choose right disjunct

Existsi(String)

Existential introduction: exists e

Clear(Vec<String>)

Clear hypotheses

Revert(Vec<String>)

Revert hypotheses

Subst(String)

Substitute a variable

Contradiction

Derive a contradiction

Exfalso

Switch to proving False

ByContra(Option<String>)

Proof by contradiction: by_contra h

Assumption

Close by assumption

Trivial

Close trivially

Rfl

Reflexivity

Intros(Vec<String>)

Intros (shorthand for intro)

Generalize(String, String)

Generalize for induction

InductionPat(String, String)

Induction on pattern

Obtain(String, Box<TacticExpr>)

Obtain hypothesis

Rcases(String, Vec<String>)

Rcases (recursive cases)

Tauto

Tauto (propositional solver)

AcRfl

Ac_rfl (associative-commutative reflexivity)

Custom(CustomTactic)

Custom tactic

Located(Box<TacticExpr>, TacticLocation)

Located tactic (for IDE support)

Trait Implementations

impl Clone for TacticExpr

fn clone(&self) -> TacticExpr

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TacticExpr

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

Formats the value using the given formatter.

impl PartialEq for TacticExpr

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