Goal simplification

Applies Sym.simp to a goal's target type, producing a simplified goal or closing it if the result is True.

inductive Lean.Meta.Sym.SimpGoalResult : Type

Result of simplifying a goal with Sym.simp.

• noProgress : SimpGoalResult

  No simplification was possible.

• closed : SimpGoalResult

  The goal was closed (simplified to True).

• goal (mvarId : MVarId) : SimpGoalResult

  The goal was simplified to a new goal.

def Lean.Meta.Sym.SimpGoalResult.toOption : SimpGoalResult → CoreM (Option MVarId)

Converts a SimpGoalResult to an optional goal. Returns none if closed, some mvarId if simplified, or throws an error if no progress.

Equations

• Lean.Meta.Sym.SimpGoalResult.noProgress.toOption = Lean.throwError (Lean.toMessageData "`Sym.simp` made no progress ")
• Lean.Meta.Sym.SimpGoalResult.closed.toOption = pure none
• (Lean.Meta.Sym.SimpGoalResult.goal mvarId).toOption = pure (some mvarId)

def Lean.Meta.Sym.SimpGoalResult.ignoreNoProgress : SimpGoalResult → MVarId → SimpGoalResult

Equations

• Lean.Meta.Sym.SimpGoalResult.noProgress.ignoreNoProgress x✝ = Lean.Meta.Sym.SimpGoalResult.goal x✝
• x✝¹.ignoreNoProgress x✝ = x✝¹

def Lean.Meta.Sym.Simp.Result.toSimpGoalResult (result : Result) (mvarId : MVarId) : SymM SimpGoalResult

Converts a Simp.Result value into SimpGoalResult.

Equations

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

def Lean.Meta.Sym.simpGoal (mvarId : MVarId) (methods : Simp.Methods := { }) (config : Simp.Config := { }) : SymM SimpGoalResult

Simplifies the target of mvarId using Sym.simp. Returns .closed if the target simplifies to True, .simp mvarId' if simplified to a new goal, or .noProgress if no simplification occurred.

This function assumed the input goal is a valid Sym goal (e.g., expressions are maximally shared).

Equations

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

def Lean.Meta.Sym.simpGoalIgnoringNoProgress (mvarId : MVarId) (methods : Simp.Methods := { }) (config : Simp.Config := { }) : SymM SimpGoalResult

Similar to simpGoal, but returns .goal mvarId if no progress was made.

Equations

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