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
• forwardMatch (m : ForwardRuleMatch) : RuleTacDescr

instance Aesop.instInhabitedRuleTacDescr : Inhabited RuleTacDescr

Equations

• Aesop.instInhabitedRuleTacDescr = { default := Aesop.RuleTacDescr.apply default default }

def Aesop.RuleTacDescr.forwardRuleMatch? : RuleTacDescr → Option ForwardRuleMatch

Equations

• (Aesop.RuleTacDescr.forwardMatch m).forwardRuleMatch? = some m
• x✝.forwardRuleMatch? = none