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.

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.

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.

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.

def Lean.MVarId.unfoldReducible (mvarId : Lean.MVarId) : Lean.MetaM Lean.MVarId

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

Equations

• mvarId.unfoldReducible = mvarId.transformTarget Lean.Meta.Grind.unfoldReducible

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

Abstract nested proofs occurring in the goal's target.

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

Beta-reduce the goal's target.

Equations

• mvarId.betaReduce = mvarId.transformTarget fun (x : Lean.Expr) => liftM (Lean.Core.betaReduce x)

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

If the target is not False, apply byContradiction.

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.