Enum LeanTactic 

pub enum LeanTactic {
    Apply(String),
    Exact(Box<LeanProofTerm>),
    Intro(Vec<String>),
    Cases(String),
    Split,
    Constructor(usize),
    Rfl,
    Simp {
        lemmas: Vec<String>,
    },
    Omega,
    Decide,
    Seq(Vec<LeanTactic>),
}

Lean 4 tactic.

Variants

Apply(String)

apply tactic

Exact(Box<LeanProofTerm>)

exact tactic

Intro(Vec<String>)

intro tactic

Cases(String)

cases tactic

Split

split tactic

Constructor(usize)

left/right tactic

Rfl

rfl (reflexivity)

Simp

simp

Fields

lemmas: Vec<String>

Omega

omega (arithmetic)

Decide

decide (decidable propositions)

Seq(Vec<LeanTactic>)

sequence of tactics

Implementations

impl LeanTactic

pub fn to_lean(&self) -> String

Convert tactic to Lean 4 syntax

Trait Implementations

impl Clone for LeanTactic

fn clone(&self) -> LeanTactic

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanTactic

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

Formats the value using the given formatter.