structure Aesop.NormM.Context : Type

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

structure Aesop.NormM.State : Type

• forwardState : ForwardState
• forwardRuleMatches : ForwardRuleMatches

instance Aesop.NormM.instInhabitedState : Inhabited State

Equations

• Aesop.NormM.instInhabitedState = { default := { forwardState := default, forwardRuleMatches := default } }

@[reducible, inline]

abbrev Aesop.NormM (α : Type) : Type

Equations

• Aesop.NormM = ReaderT Aesop.NormM.Context (StateRefT' IO.RealWorld Aesop.NormM.State Aesop.BaseM)

def Aesop.getForwardState : NormM ForwardState

Equations

• Aesop.getForwardState = do let __do_lift ← getThe Aesop.NormM.State pure __do_lift.forwardState

def Aesop.getResetForwardState : NormM ForwardState

Equations

• Aesop.getResetForwardState = modifyGetThe Aesop.NormM.State fun (s : Aesop.NormM.State) => (s.forwardState, { forwardState := ∅, forwardRuleMatches := s.forwardRuleMatches })

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• (Aesop.NormRuleResult.succeeded goal steps?).newGoal? = some goal
• (Aesop.NormRuleResult.proved steps?).newGoal? = none

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

Equations

• (Aesop.NormRuleResult.succeeded goal steps?).steps? = steps?
• (Aesop.NormRuleResult.proved steps?).steps? = steps?

def Aesop.optNormRuleResultEmoji : Option NormRuleResult → String

Equations

• Aesop.optNormRuleResultEmoji (some (Aesop.NormRuleResult.succeeded goal steps?)) = Aesop.ruleSuccessEmoji
• Aesop.optNormRuleResultEmoji (some (Aesop.NormRuleResult.proved steps?)) = Aesop.ruleProvedEmoji
• Aesop.optNormRuleResultEmoji none = Aesop.ruleFailureEmoji

@[always_inline]

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

Equations

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

def Aesop.withNormTraceNode.fmt (ruleName : DisplayRuleName) (r : Except Lean.Exception (Option NormRuleResult)) : NormM Lean.MessageData

Equations

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

def Aesop.runNormRuleTac (rule : NormRule) (input : RuleTacInput) (fs : ForwardState) (rs : LocalRuleSet) : NormM (Option (NormRuleResult × ForwardState × Array ForwardRuleMatch × 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.

Equations

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

def Aesop.runNormRuleTac.err (rule : NormRule) (input : RuleTacInput) {α : Type} (msg : Lean.MessageData) : Lean.MetaM α

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Aesop.normSimpCore.addLocalRules (goal : Lean.MVarId) (localRules : Array LocalNormSimpRule) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray) (isSimpAll : Bool) : NormM (Lean.Meta.Simp.Context × Lean.Meta.Simp.SimprocsArray)

Equations

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

@[always_inline]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Aesop.NormRuleResult.toNormSeqResult ruleName (Aesop.NormRuleResult.proved steps?) = Aesop.NormSeqResult.proved #[(ruleName, steps?)]
• Aesop.NormRuleResult.toNormSeqResult ruleName (Aesop.NormRuleResult.succeeded goal steps?) = Aesop.NormSeqResult.changed goal #[(ruleName, steps?)]

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

Equations

• Aesop.optNormRuleResultToNormSeqResult (some (ruleName, r)) = Aesop.NormRuleResult.toNormSeqResult ruleName r
• Aesop.optNormRuleResultToNormSeqResult none = Aesop.NormSeqResult.unchanged

@[reducible, inline]

abbrev Aesop.NormStep : Type

Equations

• Aesop.NormStep = (Lean.MVarId → Array (Aesop.IndexMatchResult Aesop.NormRule) → Array (Aesop.IndexMatchResult Aesop.NormRule) → Aesop.NormM Aesop.NormSeqResult)

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

Equations

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

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

Equations

• Aesop.NormStep.runPreSimpRules mvars x✝² x✝¹ x✝ = Aesop.optNormRuleResultToNormSeqResult <$> Aesop.runFirstNormRule x✝² mvars x✝¹

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

Equations

• Aesop.NormStep.runPostSimpRules mvars x✝² x✝¹ x✝ = Aesop.optNormRuleResultToNormSeqResult <$> Aesop.runFirstNormRule x✝² mvars x✝

def Aesop.NormStep.unfold : NormStep

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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