def
Aesop.expandNextGoal.fmt
{Q : Type}
[Queue Q]
(id : GoalId)
(priority : Percent)
(initialGoal : Lean.MVarId)
(initialMetaState : Lean.Meta.SavedState)
(result : Except Lean.Exception RuleResult)
:
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
This function detects whether the search has made progress, meaning that the remaining goals after safe prefix expansion are different from the initial goal. We approximate this by checking whether, after safe prefix expansion, either of the following statements is true.
- There is a safe rapp.
- A subgoal of the preprocessing rule has been modified during normalisation.
This is an approximation because a safe rule could, in principle, leave the initial goal unchanged.
Equations
Instances For
def
Aesop.throwAesopEx
{Q : Type}
[Queue Q]
{α : Type}
(mvarId : Lean.MVarId)
(remainingSafeGoals : Array Lean.MVarId)
(safePrefixExpansionSuccess : Bool)
(msg? : Option Lean.MessageData)
:
SearchM Q α
Equations
Instances For
def
Aesop.handleNonfatalError
{Q : Type}
[Queue Q]
(err : Lean.MessageData)
:
SearchM Q (Array Lean.MVarId)
Equations
Instances For
def
Aesop.search
(goal : Lean.MVarId)
(ruleSet? : Option LocalRuleSet := none)
(options : Options := { })
(simpConfig : Lean.Meta.Simp.Config := { })
(simpConfigSyntax? : Option Lean.Term := none)
(stats : Stats := ∅)
: