Documentation

Lean.Meta.Tactic.Grind.Util

source
def Lean.MVarId.ensureNoMVar (mvarId : Lean.MVarId) :
Lean.MetaM Unit

Throws an exception if target of the given goal contains metavariables.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.MVarId.ensureProp (mvarId : Lean.MVarId) :
Lean.MetaM Unit

Throws an exception if target is not a proposition.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.MVarId.transformTarget (mvarId : Lean.MVarId) (f : Lean.Expr → Lean.MetaM Lean.Expr) :
Lean.MetaM Lean.MVarId
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Grind.unfoldReducible (e : Lean.Expr) :
Lean.MetaM Lean.Expr

Unfold all reducible declarations occurring in e.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.MVarId.unfoldReducible (mvarId : Lean.MVarId) :
Lean.MetaM Lean.MVarId

Unfold all reducible declarations occurring in the goal's target.

Equations
source
def Lean.MVarId.abstractNestedProofs (mvarId : Lean.MVarId) (mainDeclName : Lake.Name) :
Lean.MetaM Lean.MVarId

Abstract nested proofs occurring in the goal's target.

Equations
source
def Lean.MVarId.betaReduce (mvarId : Lean.MVarId) :
Lean.MetaM Lean.MVarId

Beta-reduce the goal's target.

Equations
source
def Lean.MVarId.byContra? (mvarId : Lean.MVarId) :
Lean.MetaM (Option Lean.MVarId)

If the target is not False, apply byContradiction.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.MVarId.clearAuxDecls (mvarId : Lean.MVarId) :
Lean.MetaM Lean.MVarId

Clear auxiliary decls used to encode recursive declarations. grind eliminates them to ensure they are not accidentally used by its proof automation.

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