inductive Aesop.SimpResult : Type

• solved (usedTheorems : Lean.Meta.Simp.UsedSimps) : SimpResult
• unchanged : SimpResult
• simplified (newGoal : Lean.MVarId) (usedTheorems : Lean.Meta.Simp.UsedSimps) : SimpResult

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

def Aesop.addLetDeclsToSimpTheorems (ctx : Lean.Meta.Simp.Context) : Lean.MetaM Lean.Meta.Simp.Context

Add all let hypotheses in the local context as simp theorems.

Background: by default, in the goal x : _ := v ⊢ P[x], simp does not substitute x by v in the target. The simp option zetaDelta can be used to make simp perform this substitution, but we don't want to set it because then Aesop simp would diverge from default simp, so we would have to adjust the aesop? output as well. Instead, we add let hypotheses explicitly. This way, simp? picks them up as well.

See lean4#3520.

def Aesop.addLetDeclsToSimpTheoremsUnlessZetaDelta (ctx : Lean.Meta.Simp.Context) : Lean.MetaM Lean.Meta.Simp.Context

def Aesop.simpGoal (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray) (discharge? : Option Lean.Meta.Simp.Discharge := none) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array Lean.FVarId := #[]) (stats : Lean.Meta.Simp.Stats := { }) : Lean.MetaM SimpResult

def Aesop.simpGoalWithAllHypotheses (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray) (discharge? : Option Lean.Meta.Simp.Discharge := none) (simplifyTarget : Bool := true) (stats : Lean.Meta.Simp.Stats := { }) : Lean.MetaM SimpResult

def Aesop.simpAll (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray) (stats : Lean.Meta.Simp.Stats := { }) : Lean.MetaM SimpResult