Documentation

Lean.Meta.Tactic.Grind.Arith.Linear.ToExpr

ToExpr instances for Linarith.Poly types.

source
def Lean.Meta.Grind.Arith.Linear.ofPoly (p : Poly) :
Expr
Equations
    Instances For
      source
      instance Lean.Meta.Grind.Arith.Linear.instToExprPoly :
      ToExpr Poly
      Equations
        source
        def Lean.Meta.Grind.Arith.Linear.ofLinExpr (e : Grind.Linarith.Expr) :
        Expr
        Equations
          Instances For
            source
            instance Lean.Meta.Grind.Arith.Linear.instToExprExpr :
            ToExpr Grind.Linarith.Expr
            Equations