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.

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

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

Converts a Simp.Result value into SimpGoalResult.

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).

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.