inductive Aesop.RuleTacDescr : Type

• apply (term : RuleTerm) (md : Lean.Meta.TransparencyMode) : RuleTacDescr
• constructors (constructorNames : Array Lean.Name) (md : Lean.Meta.TransparencyMode) : RuleTacDescr
• forward (term : RuleTerm) (immediate : UnorderedArraySet PremiseIndex) (isDestruct : Bool) : RuleTacDescr
• cases (target : CasesTarget) (md : Lean.Meta.TransparencyMode) (isRecursiveType : Bool) (ctorNames : Array CtorNames) : RuleTacDescr
• tacticM (decl : Lean.Name) : RuleTacDescr
• ruleTac (decl : Lean.Name) : RuleTacDescr
• tacGen (decl : Lean.Name) : RuleTacDescr
• singleRuleTac (decl : Lean.Name) : RuleTacDescr
• tacticStx (stx : Lean.Syntax) : RuleTacDescr
• preprocess : RuleTacDescr
• forwardMatches (ms : Array ForwardRuleMatch) : RuleTacDescr

def Aesop.instInhabitedRuleTacDescr.default : RuleTacDescr

@[implicit_reducible]

instance Aesop.instInhabitedRuleTacDescr : Inhabited RuleTacDescr

def Aesop.RuleTacDescr.forwardRuleMatches? : RuleTacDescr → Option (Array ForwardRuleMatch)