Documentation

Lean.Meta.Tactic.Grind.Util

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
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Unfold all reducible declarations occurring in e.

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

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

          Equations
          Instances For

            Abstract nested proofs occurring in the goal's target.

            Equations
            Instances For

              Beta-reduce the goal's target.

              Equations
              Instances For

                If the target is not False, apply byContradiction.

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

                  Clear 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