Dot-notation entry points to Sym.Arith denotation, plus denotation of the solver's constraints.

def Lean.Grind.CommRing.Expr.denoteExpr' {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [Meta.Sym.Arith.MonadCanon M] [Meta.Sym.Arith.MonadRing M] (vars : Array Lean.Expr) (e : Meta.Sym.Arith.RingExpr) : M Lean.Expr

Equations

• Lean.Grind.CommRing.Expr.denoteExpr' vars e = Lean.Meta.Sym.Arith.denoteRingExpr' vars e

def Lean.Grind.CommRing.Power.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [Meta.Sym.Arith.MonadCanon M] [Meta.Sym.Arith.MonadRing M] [Meta.Sym.Arith.MonadGetVar M] (pw : Power) : M Lean.Expr

Equations

• pw.denoteExpr = Lean.Meta.Sym.Arith.denotePower pw

def Lean.Grind.CommRing.Mon.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [Meta.Sym.Arith.MonadCanon M] [Meta.Sym.Arith.MonadRing M] [Meta.Sym.Arith.MonadGetVar M] (m : Mon) : M Lean.Expr

Equations

• m.denoteExpr = Lean.Meta.Sym.Arith.denoteMon m

def Lean.Grind.CommRing.Poly.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [Meta.Sym.Arith.MonadCanon M] [Meta.Sym.Arith.MonadRing M] [Meta.Sym.Arith.MonadGetVar M] (p : Poly) : M Lean.Expr

Equations

• p.denoteExpr = Lean.Meta.Sym.Arith.denotePoly p

def Lean.Grind.CommRing.Expr.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [Meta.Sym.Arith.MonadCanon M] [Meta.Sym.Arith.MonadRing M] [Meta.Sym.Arith.MonadGetVar M] (e : Meta.Sym.Arith.RingExpr) : M Lean.Expr

Equations

• Lean.Grind.CommRing.Expr.denoteExpr e = Lean.Meta.Sym.Arith.denoteRingExpr e

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [Sym.Arith.MonadCanon M] [Sym.Arith.MonadRing M] [Sym.Arith.MonadGetVar M] (c : EqCnstr) : M Expr

Equations

• c.denoteExpr = do let __do_lift ← c.p.denoteExpr let __do_lift_1 ← Lean.Meta.Sym.Arith.denoteNum 0 Lean.Meta.Grind.Arith.CommRing.mkEq✝ __do_lift __do_lift_1

def Lean.Meta.Grind.Arith.CommRing.PolyDerivation.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [Sym.Arith.MonadCanon M] [Sym.Arith.MonadRing M] [Sym.Arith.MonadGetVar M] (d : PolyDerivation) : M Expr

Equations

• d.denoteExpr = d.p.denoteExpr

def Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [Sym.Arith.MonadCanon M] [Sym.Arith.MonadRing M] [Sym.Arith.MonadGetVar M] (c : DiseqCnstr) : M Expr

Equations

• One or more equations did not get rendered due to their size.