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

Equations

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