source
inductive Aesop.RuleResult :
Type

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

Instances For

source
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

Instances For

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

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

Instances For

source
inductive Aesop.SafeRuleResult :
Type

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

Instances For

source
@[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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

source
inductive Aesop.SafeRulesResult :
Type

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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For