This module contains helpers useful to prove unfolding and/or equational theorems.

source
def Lean.Elab.Eqns.simpMatch? (mvarId : MVarId) :
MetaM (Option MVarId)
Equations

- Lean.Elab.Eqns.simpMatch? mvarId = do let mvarId' ← Lean.Meta.Split.simpMatchTarget mvarId if (mvarId != mvarId') = true then pure (some mvarId') else pure none

Instances For

source
def Lean.Elab.Eqns.simpIf? (mvarId : MVarId) (useNewSemantics : Bool := false) :
MetaM (Option MVarId)

Simplify `if-then-expression`s in the goal target. If `useNewSemantics` is `true`, the flag `backward.split` is ignored.

Equations

- Lean.Elab.Eqns.simpIf? mvarId useNewSemantics = do let mvarId' ← Lean.Meta.simpIfTarget mvarId true useNewSemantics if (mvarId != mvarId') = true then pure (some mvarId') else pure none

Instances For

source
def Lean.Elab.Eqns.tryURefl (mvarId : MVarId) :
MetaM Bool

Try to close goal using `rfl` with smart unfolding turned off.

Equations

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

Instances For

source
def Lean.Elab.Eqns.deltaLHS (mvarId : MVarId) :
MetaM MVarId

Delta reduce the equation left-hand-side

Equations

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

Instances For

source
def Lean.Elab.Eqns.tryContradiction (mvarId : MVarId) :
MetaM Bool
Equations

- Lean.Elab.Eqns.tryContradiction mvarId = mvarId.contradictionCore { genDiseq := true }

Instances For

source
def Lean.Elab.Eqns.whnfReducibleLHS? (mvarId : MVarId) :
MetaM (Option MVarId)

Apply `whnfR` to lhs, return `none` if `lhs` was not modified

Equations

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

Instances For