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

Instances For

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

Instances For

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

Instances For

source
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)

Instances For

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

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

source
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)

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Converts nested `Expr.proj`s into projection applications if possible.

Equations

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

Instances For

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

Instances For

source
@[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.

source
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

Instances For

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

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

Instances For

source
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

Instances For

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

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

Instances For

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

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

Instances For

source
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

Instances For

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

Instances For

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

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

Instances For

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

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

Instances For

source
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!

Instances For