← Mathematical handbook

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

@[instance_reducible]

instance Aesop.instInhabitedRuleTacDescr : Inhabited RuleTacDescr

Equations

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

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

Equations

• (Aesop.RuleTacDescr.forwardMatches ms).forwardRuleMatches? = some ms
• x✝.forwardRuleMatches? = none