Documentation

Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename

source
def Lean.Grind.CommRing.Power.renameVars (pw : Power) (f : Meta.Grind.VarRename) :
Power
Equations
    Instances For
      source
      def Lean.Grind.CommRing.Mon.renameVars (m : Mon) (f : Meta.Grind.VarRename) :
      Mon
      Equations
        Instances For
          source
          def Lean.Grind.CommRing.Poly.renameVars (p : Poly) (f : Meta.Grind.VarRename) :
          Poly
          Equations
            Instances For
              source
              def Lean.Grind.CommRing.Expr.renameVars (e : Expr) (f : Meta.Grind.VarRename) :
              Expr
              Equations
                Instances For
                  source
                  def Lean.Grind.CommRing.Power.collectVars (pw : Power) :
                  Meta.Grind.VarCollector
                  Equations
                    Instances For
                      source
                      def Lean.Grind.CommRing.Mon.collectVars (m : Mon) :
                      Meta.Grind.VarCollector
                      Equations
                        Instances For
                          source
                          def Lean.Grind.CommRing.Poly.collectVars (p : Poly) :
                          Meta.Grind.VarCollector
                          Equations
                            Instances For
                              source
                              def Lean.Grind.CommRing.Expr.collectVars (e : Expr) :
                              Meta.Grind.VarCollector
                              Equations
                                Instances For