inductive Aesop.NormRuleResult : Type

• succeeded: Lean.MVarId → Except Aesop.DisplayRuleName Aesop.TacticInvocation → Aesop.NormRuleResult
• proved: Except Aesop.DisplayRuleName Aesop.TacticInvocation → Aesop.NormRuleResult
• failed: Option Aesop.TacticInvocation → Aesop.NormRuleResult

def Aesop.NormRuleResult.isSuccessful : Aesop.NormRuleResult → Bool

Equations

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

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

Equations

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

def Aesop.NormRuleResult.toEmoji : Aesop.NormRuleResult → String

Equations

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

@[always_inline]

def Aesop.withNormTraceNode (ruleName : Aesop.DisplayRuleName) (k : Lean.MetaM Aesop.NormRuleResult) : Lean.MetaM Aesop.NormRuleResult

Equations

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

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

Equations

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

def Aesop.mkNormRuleTacticInvocation (ruleName : Aesop.RuleName) (scriptBuilder? : Option Aesop.RuleTacScriptBuilder) (preGoal : Lean.MVarId) (outGoal? : Option Aesop.GoalWithMVars) (preState : Lean.Meta.SavedState) (postState : Lean.Meta.SavedState) : Lean.MetaM (Except Aesop.DisplayRuleName Aesop.TacticInvocation)

Equations

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

def Aesop.runNormRuleTac (rule : Aesop.NormRule) (input : Aesop.RuleTacInput) : Lean.MetaM Aesop.NormRuleResult

Equations

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

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

Equations

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

def Aesop.runNormRuleCore (goal : Lean.MVarId) (mvars : Aesop.UnorderedArraySet Lean.MVarId) (options : Aesop.Options') (rule : Aesop.IndexMatchResult Aesop.NormRule) : Lean.MetaM Aesop.NormRuleResult

Equations

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

def Aesop.runNormRule (goal : Lean.MVarId) (mvars : Aesop.UnorderedArraySet Lean.MVarId) (options : Aesop.Options') (rule : Aesop.IndexMatchResult Aesop.NormRule) : Aesop.ProfileT Lean.MetaM Aesop.NormRuleResult

Equations

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

def Aesop.runFirstNormRule (goal : Lean.MVarId) (mvars : Aesop.UnorderedArraySet Lean.MVarId) (options : Aesop.Options') (rules : Array (Aesop.IndexMatchResult Aesop.NormRule)) : Aesop.ProfileT Lean.MetaM Aesop.NormRuleResult

Equations

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

def Aesop.mkNormSimpScriptStep (ctx : Aesop.NormSimpContext) (preGoal : Lean.MVarId) (postGoal? : Option Aesop.GoalWithMVars) (preState : Lean.Meta.SavedState) (postState : Lean.Meta.SavedState) (usedTheorems : Lean.Meta.Simp.UsedSimps) : Lean.MetaM Aesop.TacticInvocation

Equations

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

def Aesop.SimpResult.toNormRuleResult (ruleName : Aesop.DisplayRuleName) (ctx : Aesop.NormSimpContext) (originalGoal : Aesop.GoalWithMVars) (preState : Lean.Meta.SavedState) (postState : Lean.Meta.SavedState) (generateScript : Bool) : Aesop.SimpResult → Lean.MetaM Aesop.NormRuleResult

Equations

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

@[always_inline]

def Aesop.SimpResult.toNormRuleResult.mkScriptStep? (ruleName : Aesop.DisplayRuleName) (ctx : Aesop.NormSimpContext) (originalGoal : Aesop.GoalWithMVars) (preState : Lean.Meta.SavedState) (postState : Lean.Meta.SavedState) (generateScript : Bool) (newGoal? : Option Lean.MVarId) (usedTheorems : Lean.Meta.Simp.UsedSimps) : Lean.MetaM (Except Aesop.DisplayRuleName Aesop.TacticInvocation)

Equations

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

def Aesop.normSimpCore (ctx : Aesop.NormSimpContext) (localSimpRules : Array Aesop.LocalNormSimpRule) (goal : Lean.MVarId) (goalMVars : Lean.HashSet Lean.MVarId) (generateScript : Bool) : Lean.MetaM Aesop.NormRuleResult

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 : Lean.MetaM Aesop.NormRuleResult) : Lean.MetaM Aesop.NormRuleResult

Equations

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

def Aesop.checkedNormSimpCore (ctx : Aesop.NormSimpContext) (localSimpRules : Array Aesop.LocalNormSimpRule) (goal : Lean.MVarId) (goalMVars : Lean.HashSet Lean.MVarId) (generateScript : Bool) : Lean.MetaM Aesop.NormRuleResult

Equations

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

def Aesop.normSimp (ctx : Aesop.NormSimpContext) (localSimpRules : Array Aesop.LocalNormSimpRule) (goal : Lean.MVarId) (goalMVars : Lean.HashSet Lean.MVarId) (generateScript : Bool) : Aesop.ProfileT Lean.MetaM Aesop.NormRuleResult

Equations

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

def Aesop.normUnfoldCore (unfoldRules : Lean.PHashMap Lean.Name (Option Lean.Name)) (goal : Lean.MVarId) (goalMVars : Lean.HashSet Lean.MVarId) (generateScript : Bool) : Lean.MetaM Aesop.NormRuleResult

Equations

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

def Aesop.checkedNormUnfoldCore (unfoldRules : Lean.PHashMap Lean.Name (Option Lean.Name)) (goal : Lean.MVarId) (goalMVars : Lean.HashSet Lean.MVarId) (generateScript : Bool) : Lean.MetaM Aesop.NormRuleResult

Equations

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

def Aesop.normUnfold (unfoldRules : Lean.PHashMap Lean.Name (Option Lean.Name)) (goal : Lean.MVarId) (goalMVars : Lean.HashSet Lean.MVarId) (generateScript : Bool) : Aesop.ProfileT Lean.MetaM Aesop.NormRuleResult

Equations

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

inductive Aesop.NormSeqResult : Type

• proved: Except Aesop.DisplayRuleName Aesop.UnstructuredScript → Aesop.NormSeqResult
• unproved: Lean.MVarId → Except Aesop.DisplayRuleName Aesop.UnstructuredScript → Aesop.NormSeqResult

@[inline, reducible]

abbrev Aesop.NormStep : Type

Equations

• Aesop.NormStep = (Lean.MVarId → Array (Aesop.IndexMatchResult Aesop.NormRule) → Array (Aesop.IndexMatchResult Aesop.NormRule) → Aesop.ProfileT Lean.MetaM Aesop.NormRuleResult)

def Aesop.runNormSteps (rs : Aesop.RuleSet) (goal : Lean.MVarId) (maxIterations : Nat) (steps : Array Aesop.NormStep) (stepsNe : 0 < Array.size steps) : Aesop.ProfileT Lean.MetaM Aesop.NormSeqResult

Equations

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

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

Equations

• Aesop.NormStep.runPreSimpRules options mvars x x x = match x, x, x with | goal, preSimpRules, x => Aesop.runFirstNormRule goal mvars options preSimpRules

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

Equations

• Aesop.NormStep.runPostSimpRules options mvars x x x = match x, x, x with | goal, x, postSimpRules => Aesop.runFirstNormRule goal mvars options postSimpRules

def Aesop.NormStep.unfold (rs : Aesop.RuleSet) (options : Aesop.Options') (mvars : Lean.HashSet Lean.MVarId) : Aesop.NormStep

Equations

• Aesop.NormStep.unfold rs options mvars x x x = match x, x, x with | goal, x, x_1 => Aesop.normUnfold rs.unfoldRules goal mvars options.generateScript

def Aesop.NormStep.simp (rs : Aesop.RuleSet) (ctx : Aesop.NormSimpContext) (options : Aesop.Options') (mvars : Lean.HashSet Lean.MVarId) : Aesop.NormStep

Equations

• Aesop.NormStep.simp rs ctx options mvars x x x = match x, x, x with | goal, x, x_1 => Aesop.normSimp ctx rs.localNormSimpLemmas goal mvars options.generateScript

def Aesop.normalizeGoalMVar (rs : Aesop.RuleSet) (normSimpContext : Aesop.NormSimpContext) (options : Aesop.Options') (goal : Lean.MVarId) (mvars : Aesop.UnorderedArraySet Lean.MVarId) : Aesop.ProfileT Lean.MetaM Aesop.NormSeqResult

Equations

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

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

Equations

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