inductive Aesop.RuleResult : Type

• proved: Array Aesop.RappRef → Aesop.RuleResult
• succeeded: Array Aesop.RappRef → Aesop.RuleResult
• failed: Aesop.RuleResult

def Aesop.RuleResult.toEmoji : Aesop.RuleResult → String

Equations

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

def Aesop.RuleResult.isSuccessful : Aesop.RuleResult → Bool

Equations

• Aesop.RuleResult.isSuccessful x = match x with | Aesop.RuleResult.proved newRapps => true | Aesop.RuleResult.succeeded newRapps => true | Aesop.RuleResult.failed => false

inductive Aesop.SafeRuleResult : Type

• regular: Aesop.RuleResult → Aesop.SafeRuleResult
• postponed: Aesop.PostponedSafeRule → Aesop.SafeRuleResult

def Aesop.SafeRuleResult.toEmoji : Aesop.SafeRuleResult → String

Equations

• Aesop.SafeRuleResult.toEmoji x = match x with | Aesop.SafeRuleResult.regular r => Aesop.RuleResult.toEmoji r | Aesop.SafeRuleResult.postponed result => Aesop.rulePostponedEmoji

def Aesop.SafeRuleResult.isSuccessfulOrPostponed : Aesop.SafeRuleResult → Bool

Equations

• Aesop.SafeRuleResult.isSuccessfulOrPostponed x = match x with | Aesop.SafeRuleResult.regular r => Aesop.RuleResult.isSuccessful r | Aesop.SafeRuleResult.postponed result => true

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

Equations

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

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

Equations

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

@[always_inline]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

inductive Aesop.SafeRulesResult : Type

• proved: Array Aesop.RappRef → Aesop.SafeRulesResult
• succeeded: Array Aesop.RappRef → Aesop.SafeRulesResult
• failed: Array Aesop.PostponedSafeRule → Aesop.SafeRulesResult
• skipped: Aesop.SafeRulesResult

def Aesop.SafeRulesResult.toEmoji : Aesop.SafeRulesResult → String

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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