inductive Aesop.RuleResult : Type

• proved (newRapps : Array RappRef) : RuleResult
• succeeded (newRapps : Array RappRef) : RuleResult
• failed : RuleResult

def Aesop.RuleResult.toEmoji : RuleResult → String

def Aesop.RuleResult.isSuccessful : RuleResult → Bool

inductive Aesop.SafeRuleResult : Type

• regular (result : RuleResult) : SafeRuleResult
• postponed (result : PostponedSafeRule) : SafeRuleResult

def Aesop.SafeRuleResult.toEmoji : SafeRuleResult → String

def Aesop.SafeRuleResult.isSuccessfulOrPostponed : SafeRuleResult → Bool

def Aesop.runRegularRuleTac (goal : Goal) (tac : RuleTac) (ruleName : RuleName) (indexMatchLocations : Std.HashSet IndexMatchLocation) (patternSubsts? : Option (Std.HashSet Substitution)) (options : Options') (hypTypes : Lean.PHashSet RPINF) : BaseM (Except Lean.Exception RuleTacOutput)

def Aesop.addRapps {Q : Type} [Queue Q] (parentRef : GoalRef) (rule : RegularRule) (rapps : Array RuleApplication) : SearchM Q RuleResult

@[always_inline]

def Aesop.withRuleTraceNode {Q : Type} [Queue Q] {α : Type} (ruleName : RuleName) (toEmoji : α → String) (suffix : String) (k : SearchM Q α) : SearchM Q α

def Aesop.withRuleTraceNode.fmt {Q : Type} [Queue Q] {α : Type} (ruleName : RuleName) (toEmoji : α → String) (suffix : String) (result : Except Lean.Exception α) : SearchM Q Lean.MessageData

def Aesop.runRegularRuleCore {Q : Type} [Queue Q] (parentRef : GoalRef) (rule : RegularRule) (indexMatchLocations : Std.HashSet IndexMatchLocation) (patternSubsts? : Option (Std.HashSet Substitution)) : SearchM Q (Option RuleTacOutput)

def Aesop.runSafeRule {Q : Type} [Queue Q] (parentRef : GoalRef) (matchResult : IndexMatchResult SafeRule) : SearchM Q SafeRuleResult

def Aesop.runUnsafeRule {Q : Type} [Queue Q] (parentRef : GoalRef) (matchResult : IndexMatchResult UnsafeRule) : SearchM Q RuleResult

inductive Aesop.SafeRulesResult : Type

• proved (newRapps : Array RappRef) : SafeRulesResult
• succeeded (newRapps : Array RappRef) : SafeRulesResult
• failed (postponed : Array PostponedSafeRule) : SafeRulesResult
• skipped : SafeRulesResult

def Aesop.SafeRulesResult.toEmoji : SafeRulesResult → String

def Aesop.runFirstSafeRule {Q : Type} [Queue Q] (gref : GoalRef) : SearchM Q SafeRulesResult

def Aesop.applyPostponedSafeRule {Q : Type} [Queue Q] (r : PostponedSafeRule) (parentRef : GoalRef) : SearchM Q RuleResult

def Aesop.runFirstUnsafeRule {Q : Type} [Queue Q] (postponedSafeRules : Array PostponedSafeRule) (parentRef : GoalRef) : SearchM Q RuleResult

partial def Aesop.runFirstUnsafeRule.loop {Q : Type} [Queue Q] (parentRef : GoalRef) (queue : UnsafeQueue) : SearchM Q (UnsafeQueue × RuleResult)

def Aesop.expandGoal {Q : Type} [Queue Q] (gref : GoalRef) : SearchM Q RuleResult

def Aesop.expandGoal.doUnsafe {Q : Type} [Queue Q] (gref : GoalRef) (postponedSafeRules : Array PostponedSafeRule) : SearchM Q RuleResult

def Aesop.expandGoal.fmtNorm {Q : Type} [Queue Q] (result : Except Lean.Exception Bool) : SearchM Q Lean.MessageData

def Aesop.expandGoal.fmtSafe {Q : Type} [Queue Q] (result : Except Lean.Exception SafeRulesResult) : SearchM Q Lean.MessageData

def Aesop.expandGoal.fmtUnsafe {Q : Type} [Queue Q] (result : Except Lean.Exception RuleResult) : SearchM Q Lean.MessageData