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)
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.

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

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

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

        Delta reduce the equation left-hand-side

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

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

            Instances For