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

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

def Aesop.RuleResult.isSuccessful : Aesop.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: Aesop.RuleResult → Aesop.SafeRuleResult
• postponed: Aesop.PostponedSafeRule → Aesop.SafeRuleResult

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

Equations

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

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

Equations

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

def Aesop.runRegularRuleTac (goal : Aesop.Goal) (tac : Aesop.RuleTac) (ruleName : Aesop.RuleName) (indexMatchLocations : Std.HashSet Aesop.IndexMatchLocation) (patternInstantiations : Std.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

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 : Std.HashSet Aesop.IndexMatchLocation) (patternInstantiations : Std.HashSet Aesop.RulePatternInstantiation) : Aesop.SearchM Q (Option Aesop.RuleTacOutput)

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.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

• (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} [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)

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

Equations

• Aesop.expandGoal.fmtNorm (Except.error a) = pure (Lean.toMessageData "" ++ Lean.toMessageData Aesop.ruleErrorEmoji ++ Lean.toMessageData " Normalisation")
• Aesop.expandGoal.fmtNorm (Except.ok true) = pure (Lean.toMessageData "" ++ Lean.toMessageData Aesop.ruleProvedEmoji ++ Lean.toMessageData " Normalisation")
• Aesop.expandGoal.fmtNorm (Except.ok false) = pure (Lean.toMessageData "" ++ Lean.toMessageData Aesop.ruleSuccessEmoji ++ Lean.toMessageData " Normalisation")

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.