def Aesop.RuleTacDescr.run : RuleTacDescr → RuleTac

Equations

• (Aesop.RuleTacDescr.apply t md).run = Aesop.RuleTac.apply t md
• (Aesop.RuleTacDescr.constructors cs md).run = Aesop.RuleTac.applyConsts cs md
• (Aesop.RuleTacDescr.forward t immediate clear).run = Aesop.RuleTac.forward t immediate clear
• (Aesop.RuleTacDescr.cases target md isRecursiveType ctorNames).run = Aesop.RuleTac.cases target md isRecursiveType ctorNames
• (Aesop.RuleTacDescr.tacticM decl).run = Aesop.RuleTac.tacticM decl
• (Aesop.RuleTacDescr.singleRuleTac decl).run = Aesop.RuleTac.singleRuleTac decl
• (Aesop.RuleTacDescr.ruleTac decl).run = Aesop.RuleTac.ruleTac decl
• (Aesop.RuleTacDescr.tacticStx stx).run = Aesop.RuleTac.tacticStx stx
• (Aesop.RuleTacDescr.tacGen decl).run = Aesop.RuleTac.tacGen decl
• Aesop.RuleTacDescr.preprocess.run = Aesop.RuleTac.preprocess
• (Aesop.RuleTacDescr.forwardMatches m).run = Aesop.RuleTac.forwardMatches m