Enum CoqTacticExt 

pub enum CoqTacticExt {
    Intro(Vec<String>),
    Apply(String),
    Exact(String),
    Rewrite(bool, String),
    Simpl,
    Ring,
    Omega,
    Lia,
    Lra,
    Auto,
    EAuto,
    Tauto,
    Constructor,
    Split,
    Left,
    Right,
    Exists(String),
    Induction(String),
    Destruct(String),
    Inversion(String),
    Reflexivity,
    Symmetry,
    Transitivity(String),
    Unfold(Vec<String>),
    Fold(Vec<String>),
    Assumption,
    Contradiction,
    Exfalso,
    Clear(Vec<String>),
    Rename(String, String),
    Trivial,
    Discriminate,
    Injection(String),
    FApply(String),
    Subst(Option<String>),
    Custom(String),
}

Coq tactic

Variants

Intro(Vec<String>)

Apply(String)

Exact(String)

Rewrite(bool, String)

Simpl

Ring

Omega

Lia

Lra

Auto

EAuto

Tauto

Constructor

Split

Left

Right

Exists(String)

Induction(String)

Destruct(String)

Inversion(String)

Reflexivity

Symmetry

Transitivity(String)

Unfold(Vec<String>)

Fold(Vec<String>)

Assumption

Contradiction

Exfalso

Clear(Vec<String>)

Rename(String, String)

Trivial

Discriminate

Injection(String)

FApply(String)

Subst(Option<String>)

Custom(String)

Trait Implementations

impl Clone for CoqTacticExt

fn clone(&self) -> CoqTacticExt

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CoqTacticExt

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

Formats the value using the given formatter.

impl Display for CoqTacticExt

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

Formats the value using the given formatter.