def Aesop.runRuleTac (tac : Aesop.RuleTac) (ruleName : Aesop.RuleName) (preState : Lean.Meta.SavedState) (input : Aesop.RuleTacInput) : Lean.MetaM (Lean.Exception ⊕ Aesop.RuleTacOutput)

Equations

• One or more equations did not get rendered due to their size.