def Lean.MVarId.ensureNoMVar (mvarId : MVarId) : 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.abstractMVars (mvarId : MVarId) : MetaM MVarId

Abstracts metavariables occurring in the target.

Equations

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

def Lean.MVarId.transformTarget (mvarId : MVarId) (f : Expr → MetaM Expr) : MetaM MVarId

Equations

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

def Lean.Meta.Grind.isGrindGadget (declName : Name) : Bool

Returns true if declName is the name of a grind helper declaration that should not be unfolded by unfoldReducible.

Equations

• Lean.Meta.Grind.isGrindGadget declName = (declName == `Lean.Grind.EqMatch)

def Lean.Meta.Grind.isUnfoldReducibleTarget (e : Expr) : CoreM Bool

Equations

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

def Lean.Meta.Grind.unfoldReducibleStep (e : Expr) : MetaM TransformStep

Auxiliary function for implementing unfoldReducible and unfoldReducibleSimproc. Performs a single step.

Equations

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

def Lean.Meta.Grind.unfoldReducible (e : Expr) : MetaM 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 : MVarId) : MetaM MVarId

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

Equations

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

def Lean.MVarId.betaReduce (mvarId : MVarId) : MetaM 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 : MVarId) : MetaM (Option 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.clearImplDetails (mvarId : MVarId) : MetaM MVarId

Clears auxiliary and implementation detail decls used to encode recursive declarations and implementation details.

• grind eliminates auxiliary declarations to ensure they are not accidentally used by its proof automation.
• grind eliminates implementation detail declarations because they have a support role.

Equations

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

def Lean.Meta.Grind.eraseIrrelevantMData (e : Expr) : CoreM 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.lam children. Recall that we still have to process Expr.forallE because of ForallProp.lean. Moreover, we may not want to reduce p → q to ¬p ∨ q when (p q : Prop).

Equations

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

def Lean.Meta.Grind.foldProjs (e : Expr) : MetaM 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 : Expr) : CoreM Expr

Normalizes universe levels in constants and sorts.

Equations

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

@[extern lean_grind_normalize]

opaque Lean.Meta.Grind.normalize (e : Expr) (config : Grind.Config) : MetaM Expr

Normalizes the given expression using the grind simplification theorems and simprocs. This function is used for normalizing E-matching patterns. Note that it does not return a proof.

def Lean.Meta.Grind.markAsMatchCond (e : Expr) : Expr

Returns Grind.MatchCond e. We have special support for propagating is truth value. See comment at MatchCond.lean.

Equations

• Lean.Meta.Grind.markAsMatchCond e = Lean.mkApp (Lean.mkConst `Lean.Grind.MatchCond) e

def Lean.Meta.Grind.isMatchCond (e : Expr) : Bool

Equations

• Lean.Meta.Grind.isMatchCond e = e.isAppOfArity `Lean.Grind.MatchCond 1

def Lean.Meta.Grind.markAsPreMatchCond (e : Expr) : Expr

Returns Grind.PreMatchCond e. Recall that Grind.PreMatchCond is an identity function, but the simproc reducePreMatchCond is used to prevent the term e from being simplified. Grind.PreMatchCond is later converted into Grind.MatchCond. See comment at MatchCond.lean.

Equations

• Lean.Meta.Grind.markAsPreMatchCond e = Lean.mkApp (Lean.mkConst `Lean.Grind.PreMatchCond) e

def Lean.Meta.Grind.isPreMatchCond (e : Expr) : Bool

Equations

• Lean.Meta.Grind.isPreMatchCond e = e.isAppOfArity `Lean.Grind.PreMatchCond 1

def Lean.Meta.Grind.reducePreMatchCond : Simp.DSimproc

Equations

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

def Lean.Meta.Grind.addPreMatchCondSimproc (s : Simprocs) : CoreM Simprocs

Adds reducePreMatchCond to s

Equations

• Lean.Meta.Grind.addPreMatchCondSimproc s = s.add `Lean.Meta.Grind.reducePreMatchCond false

def Lean.Meta.Grind.replacePreMatchCond (e : Expr) : MetaM Simp.Result

Converts Grind.PreMatchCond into Grind.MatchCond. Recall that Grind.PreMatchCond uses default reducibility setting, but Grind.MatchCond does not.

Equations

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

def Lean.Meta.Grind.isIte (e : Expr) : Bool

Equations

• Lean.Meta.Grind.isIte e = (e.isAppOf `ite && decide (e.getAppNumArgs ≥ 5))

def Lean.Meta.Grind.isDIte (e : Expr) : Bool

Equations

• Lean.Meta.Grind.isDIte e = (e.isAppOf `dite && decide (e.getAppNumArgs ≥ 5))

def Lean.Meta.Grind.getBinOp (e : Expr) : Option Expr

Equations

• Lean.Meta.Grind.getBinOp e = if (!e.isApp) = true then none else have f := e.appFn!; if (!f.isApp) = true then none else some f.appFn!