structure Aesop.NormM.Context : Type

• options : Options'
• ruleSet : LocalRuleSet
• normSimpContext : NormSimpContext

structure Aesop.NormM.State : Type

• forwardState : ForwardState
• forwardRuleMatches : ForwardRuleMatches

@[implicit_reducible]

instance Aesop.NormM.instInhabitedState : Inhabited State

def Aesop.NormM.instInhabitedState.default : State

@[reducible, inline]

abbrev Aesop.NormM (α : Type) : Type

def Aesop.getForwardState : NormM ForwardState

def Aesop.getResetForwardState : NormM ForwardState

def Aesop.modifyForwardState (fs : ForwardState) (newMatches : Array ForwardRuleMatch) (erasedHyps : Std.HashSet Lean.FVarId) : NormM Unit

def Aesop.updateForwardState (goal : Lean.MVarId) : NormM Unit

def Aesop.eraseForwardRuleMatch (m : ForwardRuleMatch) : NormM Unit

def Aesop.applyDiffToForwardState (diff : GoalDiff) : NormM Unit

inductive Aesop.NormRuleResult : Type

• succeeded (goal : Lean.MVarId) (steps? : Option (Array Script.LazyStep)) : NormRuleResult
• proved (steps? : Option (Array Script.LazyStep)) : NormRuleResult

def Aesop.NormRuleResult.newGoal? : NormRuleResult → Option Lean.MVarId

def Aesop.NormRuleResult.steps? : NormRuleResult → Option (Array Script.LazyStep)

def Aesop.optNormRuleResultEmoji : Option NormRuleResult → String

@[always_inline]

def Aesop.withNormTraceNode (ruleName : DisplayRuleName) (k : NormM (Option NormRuleResult)) : NormM (Option NormRuleResult)

def Aesop.runNormRuleTac (rule : NormRule) (input : RuleTacInput) (fs : ForwardState) (rs : LocalRuleSet) : NormM (Option (NormRuleResult × ForwardState × Std.HashSet Lean.FVarId) × Array ForwardRuleMatch)

On success, returns the rule tactic's result, the new forward state and the new forward rule matches. If rule corresponds to some forward rule matches, returns the matches as well.

def Aesop.runNormRule (goal : Lean.MVarId) (mvars : UnorderedArraySet Lean.MVarId) (rule : IndexMatchResult NormRule) : NormM (Option NormRuleResult)

def Aesop.runFirstNormRule (goal : Lean.MVarId) (mvars : UnorderedArraySet Lean.MVarId) (rules : Array (IndexMatchResult NormRule)) : NormM (Option (DisplayRuleName × NormRuleResult))

def Aesop.mkNormSimpScriptStep (preGoal : Lean.MVarId) (postGoal? : Option Lean.MVarId) (preState postState : Lean.Meta.SavedState) (usedTheorems : Lean.Meta.Simp.UsedSimps) : NormM Script.LazyStep

def Aesop.normSimpCore (goal : Lean.MVarId) (goalMVars : Std.HashSet Lean.MVarId) : NormM (Option NormRuleResult)

@[always_inline]

def Aesop.checkSimp (name : String) (mayCloseGoal : Bool) (goal : Lean.MVarId) (x : NormM (Option NormRuleResult)) : NormM (Option NormRuleResult)

def Aesop.normSimp (goal : Lean.MVarId) (goalMVars : Std.HashSet Lean.MVarId) : NormM (Option NormRuleResult)

def Aesop.normUnfoldCore (goal : Lean.MVarId) : NormM (Option NormRuleResult)

def Aesop.normUnfold (goal : Lean.MVarId) : NormM (Option NormRuleResult)

inductive Aesop.NormSeqResult : Type

• proved (script : Array (DisplayRuleName × Option (Array Script.LazyStep))) : NormSeqResult
• changed (goal : Lean.MVarId) (script : Array (DisplayRuleName × Option (Array Script.LazyStep))) : NormSeqResult
• unchanged : NormSeqResult

def Aesop.NormRuleResult.toNormSeqResult (ruleName : DisplayRuleName) : NormRuleResult → NormSeqResult

def Aesop.optNormRuleResultToNormSeqResult : Option (DisplayRuleName × NormRuleResult) → NormSeqResult

@[reducible, inline]

abbrev Aesop.NormStep : Type

def Aesop.runNormSteps (goal : Lean.MVarId) (steps : Array NormStep) (stepsNe : 0 < steps.size) : NormM NormSeqResult

def Aesop.NormStep.runPreSimpRules (mvars : UnorderedArraySet Lean.MVarId) : NormStep

def Aesop.NormStep.runPostSimpRules (mvars : UnorderedArraySet Lean.MVarId) : NormStep

def Aesop.NormStep.unfold : NormStep

def Aesop.NormStep.simp (mvars : Std.HashSet Lean.MVarId) : NormStep

def Aesop.normalizeGoalMVar (goal : Lean.MVarId) (mvars : UnorderedArraySet Lean.MVarId) : NormM NormSeqResult

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