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

Equations

• (Aesop.SimpResult.solved usedTheorems).newGoal? = none
• Aesop.SimpResult.unchanged.newGoal? = none
• (Aesop.SimpResult.simplified g usedTheorems).newGoal? = some g

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.

Equations

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

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

Equations

• Aesop.addLetDeclsToSimpTheoremsUnlessZetaDelta ctx = if ctx.config.zetaDelta = true then pure ctx else Aesop.addLetDeclsToSimpTheorems ctx

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 := { usedTheorems := { map := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } } }) : Lean.MetaM 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? : Option Lean.Meta.Simp.Discharge := none) (simplifyTarget : Bool := true) (stats : Lean.Meta.Simp.Stats := { usedTheorems := { map := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } } }) : Lean.MetaM 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) (stats : Lean.Meta.Simp.Stats := { usedTheorems := { map := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } } }) : Lean.MetaM SimpResult

Equations

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