Throws an exception if target of the given goal contains metavariables.
Equations
Instances For
Abstracts metavariables occurring in the target.
Equations
Instances For
Returns true
if declName
is the name of a grind helper declaration that
should not be unfolded by unfoldReducible
.
Equations
Instances For
Unfolds all reducible
declarations occurring in e
.
Equations
Instances For
Unfolds all reducible
declarations occurring in the goal's target.
Equations
Instances For
Beta-reduces the goal's target.
Equations
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
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
Instances For
Converts nested Expr.proj
s into projection applications if possible.
Equations
Instances For
Normalizes universe levels in constants and sorts.
Equations
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.
Returns Grind.MatchCond e
.
We have special support for propagating is truth value.
See comment at MatchCond.lean
.
Equations
Instances For
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
Instances For
Converts Grind.PreMatchCond
into Grind.MatchCond
.
Recall that Grind.PreMatchCond
uses default reducibility setting, but
Grind.MatchCond
does not.