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

Unfolds 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

Unfolds 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

Abstracts nested proofs occurring in the goal's target.

Equations

• mvarId.abstractNestedProofs mainDeclName = mvarId.transformTarget (Lean.Meta.abstractNestedProofs mainDeclName)

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

Beta-reduces 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, applies byContradiction.

Equations

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

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

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

def Lean.Meta.Grind.eraseIrrelevantMData (e : Lean.Expr) : Lean.CoreM Lean.Expr

In the grind tactic, during Expr internalization, we don't expect to find Expr.mdata. This function ensures Expr.mdata is not found during internalization. Recall that we do not internalize Expr.forallE and Expr.lam components.

Equations

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

def Lean.Meta.Grind.foldProjs (e : Lean.Expr) : Lean.MetaM Lean.Expr

Converts nested Expr.projs into projection applications if possible.

Equations

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

def Lean.Meta.Grind.normalizeLevels (e : Lean.Expr) : Lean.CoreM Lean.Expr

Normalizes universe levels in constants and sorts.

Equations

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