Documentation

Lean.Meta.Sym.Arith.ToExpr

ToExpr instances for CommRing.Poly types.

source
def Lean.Meta.Sym.Arith.ofPower (p : Power) :
Expr
Instances For
    source
    @[implicit_reducible]
    instance Lean.Meta.Sym.Arith.instToExprPower :
    ToExpr Power
    source
    def Lean.Meta.Sym.Arith.ofMon (m : Mon) :
    Expr
    Instances For
      source
      @[implicit_reducible]
      instance Lean.Meta.Sym.Arith.instToExprMon :
      ToExpr Mon
      source
      def Lean.Meta.Sym.Arith.ofPoly (p : Poly) :
      Expr
      Instances For
        source
        @[implicit_reducible]
        instance Lean.Meta.Sym.Arith.instToExprPoly :
        ToExpr Poly
        source
        def Lean.Meta.Sym.Arith.ofRingExpr (e : Grind.CommRing.Expr) :
        Expr
        Instances For
          source
          @[implicit_reducible]
          instance Lean.Meta.Sym.Arith.instToExprExpr :
          ToExpr Grind.CommRing.Expr