Documentation

Lean.Meta.Sym.DSimp.Reduce

source
def Lean.Meta.Sym.DSimp.beta :
DSimproc
Instances For
    source
    def Lean.Meta.Sym.DSimp.zetaDelta (s : FVarIdSet) :
    DSimproc

    Unfolds the let-bound free variables in s at head position. See Sym.reduceZetaDelta?.

    Instances For
      source
      def Lean.Meta.Sym.DSimp.zetaDeltaAll :
      DSimproc
      Instances For
        source
        def Lean.Meta.Sym.DSimp.zeta :
        DSimproc
        Instances For
          source
          def Lean.Meta.Sym.DSimp.dsimpProj :
          DSimproc
          Instances For
            source
            def Lean.Meta.Sym.DSimp.dsimpMatch :
            DSimproc
            Instances For
              source
              def Lean.Meta.Sym.DSimp.unfold (declNames : NameSet) :
              DSimproc

              Unfolds the applications of the definitions in declNames, like Meta.simp does for the definitions provided in simp [f]. A definition with smart unfolding support is unfolded only when its recursion argument reduces. Any other definition is unfolded only when applied to at least as many arguments as its number of leading lambdas.

              Instances For