Enum IdrisTactic 

pub enum IdrisTactic {
    Intro(String),
    Intros,
    Exact(IdrisExpr),
    Refl,
    Trivial,
    Decide,
    Rewrite(String),
    RewriteBack(String),
    Apply(String),
    Cases(String),
    Induction(String),
    Search,
    Auto,
    With(String),
    Let(String, IdrisExpr),
    Have(String, IdrisType),
    Focus(usize),
    Claim(String, IdrisType),
    Unfold(String),
    Compute,
    Normals,
    Fail(String),
    Seq(Vec<IdrisTactic>),
}

A tactic in an Idris 2 proof script.

Variants

Intro(String)

intro x — introduce a variable.

Intros

intros — introduce all variables.

Exact(IdrisExpr)

exact e — close goal with exact term.

Refl

refl — close reflexivity goal.

Trivial

trivial — close trivial goal.

Decide

decide — close decidable goal.

Rewrite(String)

rewrite h — rewrite using equality.

RewriteBack(String)

rewrite <- h — rewrite backwards.

Apply(String)

apply f — apply a function.

Cases(String)

cases x — case split on x.

Induction(String)

induction x — do induction on x.

Search

search — auto-search for a term.

Auto

auto — auto-search.

With(String)

with e — with view pattern.

Let(String, IdrisExpr)

let x = e — introduce local definition.

Have(String, IdrisType)

have x : T by tac — prove an intermediate.

Focus(usize)

focus n — focus on sub-goal n.

Claim(String, IdrisType)

claim n t — claim sub-goal.

Unfold(String)

unfold n — unfold a definition.

Compute

compute — reduce to normal form.

Normals

normals — normalize.

Fail(String)

fail msg — fail with message.

Seq(Vec<IdrisTactic>)

Sequence of tactics.

Trait Implementations

impl Clone for IdrisTactic

fn clone(&self) -> IdrisTactic

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for IdrisTactic

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

Formats the value using the given formatter.

impl Display for IdrisTactic

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

Formats the value using the given formatter.