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
Instances For
    source
    @[implicit_reducible]
    instance Lean.Meta.Grind.Arith.CommRing.instToExprPower :
    ToExpr Power
    source
    def Lean.Meta.Grind.Arith.CommRing.ofMon (m : Mon) :
    Expr
    Instances For
      source
      @[implicit_reducible]
      instance Lean.Meta.Grind.Arith.CommRing.instToExprMon :
      ToExpr Mon
      source
      def Lean.Meta.Grind.Arith.CommRing.ofPoly (p : Poly) :
      Expr
      Instances For
        source
        @[implicit_reducible]
        instance Lean.Meta.Grind.Arith.CommRing.instToExprPoly :
        ToExpr Poly
        source
        def Lean.Meta.Grind.Arith.CommRing.ofRingExpr (e : Grind.CommRing.Expr) :
        Expr
        Instances For
          source
          @[implicit_reducible]
          instance Lean.Meta.Grind.Arith.CommRing.instToExprExpr :
          ToExpr Grind.CommRing.Expr