Documentation

Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr

ToExpr instances for CommRing.Poly types.

source
def Lean.Meta.Grind.Arith.CommRing.ofPower (p : Power) :
Expr
Equations
    Instances For
      source
      instance Lean.Meta.Grind.Arith.CommRing.instToExprPower :
      ToExpr Power
      Equations
        source
        def Lean.Meta.Grind.Arith.CommRing.ofMon (m : Mon) :
        Expr
        Equations
          Instances For
            source
            instance Lean.Meta.Grind.Arith.CommRing.instToExprMon :
            ToExpr Mon
            Equations
              source
              def Lean.Meta.Grind.Arith.CommRing.ofPoly (p : Poly) :
              Expr
              Equations
                Instances For
                  source
                  instance Lean.Meta.Grind.Arith.CommRing.instToExprPoly :
                  ToExpr Poly
                  Equations
                    source
                    def Lean.Meta.Grind.Arith.CommRing.ofRingExpr (e : Grind.CommRing.Expr) :
                    Expr
                    Equations
                      Instances For
                        source
                        instance Lean.Meta.Grind.Arith.CommRing.instToExprExpr :
                        ToExpr Grind.CommRing.Expr
                        Equations
                          source
                          def Lean.Meta.Grind.Arith.CommRing.ofNullCert (nc : Grind.CommRing.NullCert) :
                          Expr
                          Equations
                            Instances For
                              source
                              instance Lean.Meta.Grind.Arith.CommRing.instToExprNullCert :
                              ToExpr Grind.CommRing.NullCert
                              Equations