Documentation

Lean.Meta.Sym.Simp.Reduce

Definitional reduction simprocs #

Sym.simp versions of the reduction steps in Lean.Meta.Sym.Reduce. The proof of each step is Eq.refl of the result, which the kernel accepts because the terms are definitionally equal.

source
def Lean.Meta.Sym.Simp.beta :
Simproc

Beta-reduces applications with a lambda head.

Instances For
    source
    def Lean.Meta.Sym.Simp.zeta :
    Simproc

    Zeta-reduces let/have telescopes.

    Instances For
      source
      def Lean.Meta.Sym.Simp.zetaDelta (s : FVarIdSet) :
      Simproc

      Unfolds the let-bound free variables in s at head position.

      Instances For
        source
        def Lean.Meta.Sym.Simp.zetaDeltaAll :
        Simproc

        Unfolds every let-bound free variable at head position.

        Instances For
          source
          def Lean.Meta.Sym.Simp.reduceProj :
          Simproc

          Reduces projection functions applied to constructors.

          Instances For
            source
            def Lean.Meta.Sym.Simp.reduceMatcher :
            Simproc

            Iota-reduces match and recursor applications whose discriminants are constructors.

            Instances For