Documentation

Lean.Meta.Tactic.Grind.Util

Throws an exception if target of the given goal contains metavariables.

Equations
    Instances For

      Abstracts metavariables occurring in the target.

      Equations
        Instances For
          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

                              If the target is not False, applies byContradiction.

                              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.projs into projection applications if possible.

                                          Equations
                                            Instances For

                                              Normalizes universe levels in constants and sorts.

                                              Equations
                                                Instances For
                                                  @[extern lean_grind_normalize]

                                                  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
                                                      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
                                                              Equations
                                                                Instances For

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

                                                                  Equations
                                                                    Instances For
                                                                      Equations
                                                                        Instances For
                                                                          Equations
                                                                            Instances For