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