- 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
Equations
- Aesop.instInhabitedRuleTacDescr = { default := Aesop.RuleTacDescr.apply default default }