structure Aesop.NormM.Context : Type

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

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) × Option ForwardRuleMatch)

On success, returns the rule tactic's result, the new forward state and the new forward rule matches. If rule corresponds to a forward rule match, returns that match 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.