Enum CoqTactic 

pub enum CoqTactic {
    Intro(Vec<String>),
    Apply(CoqTerm),
    Exact(CoqTerm),
    Simpl,
    Reflexivity,
    Rewrite(bool, CoqTerm),
    Induction(String),
    Destruct(String),
    Auto,
    Omega,
    Lia,
    Ring,
    Unfold(Vec<String>),
    Compute,
    Assumption,
    Tauto,
    Decide,
    Trivial,
    Split,
    Left,
    Right,
    Exists(CoqTerm),
    Generalize(CoqTerm),
    Specialize(CoqTerm, Vec<CoqTerm>),
    Case(CoqTerm),
    Admit,
    Custom(String),
    Sequence(Vec<CoqTactic>),
    Then(Box<CoqTactic>, Box<CoqTactic>),
}

Ltac tactic AST.

Variants

Intro(Vec<String>)

intro x y z

Apply(CoqTerm)

apply t

Exact(CoqTerm)

exact t

Simpl

simpl / simpl in *

Reflexivity

reflexivity

Rewrite(bool, CoqTerm)

rewrite [<-] h

Induction(String)

induction x

Destruct(String)

destruct x

Auto

auto

Omega

omega

Lia

lia (Linear Integer Arithmetic)

Ring

ring

Unfold(Vec<String>)

unfold f g h

Compute

compute

Assumption

assumption

Tauto

tauto

Decide

decide

Trivial

trivial

Split

split

Left

left

Right

right

Exists(CoqTerm)

exists witness

Generalize(CoqTerm)

generalize t

Specialize(CoqTerm, Vec<CoqTerm>)

specialize (f a b)

Case(CoqTerm)

case t

Admit

admit

Custom(String)

Raw / custom tactic string

Sequence(Vec<CoqTactic>)

Sequential composition: t1. t2. t3.

Then(Box<CoqTactic>, Box<CoqTactic>)

Then combinator: t1; t2 (apply t2 to all subgoals of t1)

Implementations

impl CoqTactic

pub fn emit(&self, indent: usize) -> String

Emit as an Ltac string.

Trait Implementations

impl Clone for CoqTactic

fn clone(&self) -> CoqTactic

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CoqTactic

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

Formats the value using the given formatter.

impl PartialEq for CoqTactic

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