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

• 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.simpGoal (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (simplifyTarget : optParam Bool true) (fvarIdsToSimp : optParam (Array Lean.FVarId) #[]) (usedSimps : optParam Lean.Meta.Simp.UsedSimps ∅) : Lean.MetaM Aesop.SimpResult

Equations

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

def Aesop.simpGoalWithAllHypotheses (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (simplifyTarget : optParam Bool true) (usedSimps : optParam Lean.Meta.Simp.UsedSimps ∅) : Lean.MetaM Aesop.SimpResult

Equations

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

def Aesop.simpAll (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray) (usedSimps : optParam Lean.Meta.Simp.UsedSimps ∅) : Lean.MetaM Aesop.SimpResult

Equations

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