Documentation

Lean.Elab.PreDefinition.EqnsUtils

This module contains helpers useful to prove unfolding and/or equational theorems.

source
def Lean.Elab.Eqns.simpMatch? (mvarId : MVarId) :
MetaM (Option MVarId)
Equations
    Instances For
      source
      def Lean.Elab.Eqns.simpIf? (mvarId : MVarId) (useNewSemantics : Bool := false) :
      MetaM (Option MVarId)

      Simplify if-then-expressions in the goal target. If useNewSemantics is true, the flag backward.split is ignored.

      Equations
        Instances For
          source
          def Lean.Elab.Eqns.tryURefl (mvarId : MVarId) :
          MetaM Bool

          Try to close goal using rfl with smart unfolding turned off.

          Equations
            Instances For
              source
              def Lean.Elab.Eqns.deltaLHS (mvarId : MVarId) :
              MetaM MVarId

              Delta reduce the equation left-hand-side

              Equations
                Instances For
                  source
                  def Lean.Elab.Eqns.tryContradiction (mvarId : MVarId) :
                  MetaM Bool
                  Equations
                    Instances For
                      source
                      def Lean.Elab.Eqns.whnfReducibleLHS? (mvarId : MVarId) :
                      MetaM (Option MVarId)

                      Apply whnfR to lhs, return none if lhs was not modified

                      Equations
                        Instances For