inductive Aesop.RuleResult : Type

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

def Aesop.RuleResult.toEmoji : RuleResult → String

Equations

• (Aesop.RuleResult.proved newRapps).toEmoji = Aesop.ruleProvedEmoji
• (Aesop.RuleResult.succeeded newRapps).toEmoji = Aesop.ruleSuccessEmoji
• Aesop.RuleResult.failed.toEmoji = Aesop.ruleFailureEmoji

def Aesop.RuleResult.isSuccessful : RuleResult → Bool

Equations

• (Aesop.RuleResult.proved newRapps).isSuccessful = true
• (Aesop.RuleResult.succeeded newRapps).isSuccessful = true
• Aesop.RuleResult.failed.isSuccessful = false

inductive Aesop.SafeRuleResult : Type

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

def Aesop.SafeRuleResult.toEmoji : SafeRuleResult → String

Equations

• (Aesop.SafeRuleResult.regular r).toEmoji = r.toEmoji
• (Aesop.SafeRuleResult.postponed result).toEmoji = Aesop.rulePostponedEmoji

def Aesop.SafeRuleResult.isSuccessfulOrPostponed : SafeRuleResult → Bool

Equations

• (Aesop.SafeRuleResult.regular r).isSuccessfulOrPostponed = r.isSuccessful
• (Aesop.SafeRuleResult.postponed result).isSuccessfulOrPostponed = true

def Aesop.runRegularRuleTac (goal : Goal) (tac : RuleTac) (ruleName : RuleName) (indexMatchLocations : Std.HashSet IndexMatchLocation) (patternInstantiations : Std.HashSet RulePatternInstantiation) (options : Options') : Lean.MetaM (Lean.Exception ⊕ RuleTacOutput)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

@[always_inline]

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

Equations

• Aesop.withRuleTraceNode ruleName toEmoji suffix k = Aesop.withAesopTraceNode Aesop.TraceOption.steps (Aesop.withRuleTraceNode.fmt ruleName toEmoji suffix) k

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• (Aesop.SafeRulesResult.proved newRapps).toEmoji = Aesop.ruleProvedEmoji
• (Aesop.SafeRulesResult.succeeded newRapps).toEmoji = Aesop.ruleSuccessEmoji
• (Aesop.SafeRulesResult.failed postponed).toEmoji = Aesop.ruleFailureEmoji
• Aesop.SafeRulesResult.skipped.toEmoji = Aesop.ruleSkippedEmoji

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Aesop.expandGoal.doUnsafe gref postponedSafeRules = Aesop.withAesopTraceNode Aesop.TraceOption.steps Aesop.expandGoal.fmtUnsafe (Aesop.runFirstUnsafeRule postponedSafeRules gref)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.