inductive Aesop.SimpResult : Type

• solved: Lean.Meta.Simp.UsedSimps → Aesop.SimpResult
• unchanged: Lean.MVarId → Aesop.SimpResult
• simplified: Lean.MVarId → Lean.Meta.Simp.UsedSimps → Aesop.SimpResult

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

Equations

• Aesop.SimpResult.newGoal? x = match x with | Aesop.SimpResult.solved usedTheorems => none | Aesop.SimpResult.unchanged g => some g | Aesop.SimpResult.simplified g usedTheorems => some g

def Aesop.mkSimpOnly (stx : Lean.Syntax) (usedSimps : Lean.Meta.Simp.UsedSimps) (includeFVars : Bool) : Lean.MetaM Lean.Syntax

Equations

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

def Aesop.mkNormSimpSyntax (normSimpUseHyps : Bool) (configStx? : Option Lean.Term) : Lean.MetaM Lean.Syntax.Tactic

Equations

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

def Aesop.mkNormSimpOnlySyntax (inGoal : Lean.MVarId) (normSimpUseHyps : Bool) (configStx? : Option Lean.Term) (usedTheorems : Lean.Meta.Simp.UsedSimps) : Lean.MetaM Lean.Syntax.Tactic

Equations

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

def Aesop.mkNormSimpContext (rs : Aesop.RuleSet) (simpConfig : Aesop.SimpConfig) : Lean.MetaM Lean.Meta.Simp.Context

Equations

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