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
Throws an exception if target is not a proposition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Unfolds all reducible
declarations occurring in e
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Unfolds all reducible
declarations occurring in the goal's target.
Equations
- mvarId.unfoldReducible = mvarId.transformTarget Lean.Meta.Grind.unfoldReducible
Instances For
Abstracts nested proofs occurring in the goal's target.
Equations
- mvarId.abstractNestedProofs mainDeclName = mvarId.transformTarget (Lean.Meta.abstractNestedProofs mainDeclName)
Instances For
Beta-reduces the goal's target.
Equations
- mvarId.betaReduce = mvarId.transformTarget fun (x : Lean.Expr) => liftM (Lean.Core.betaReduce x)
Instances For
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.
Instances For
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
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
Normalizes universe levels in constants and sorts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Normalizes the given expression using the grind
simplification theorems and simprocs.
This function is used for normalzing E-matching patterns. Note that it does not return a proof.