Type Alias Tactic 

pub type Tactic = Box<dyn Fn(&mut ProofState) -> Result<(), TacticError>>;

A first-class tactic: a transformation of the proof state that either makes progress (Ok) or does not apply (Err). Tactics are values, so they compose with the combinators.

Aliased Type

pub struct Tactic(/* private fields */);