Documentation

Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr

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

source
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
Instances For
    source
    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
    Instances For
      source
      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
      Instances For
        source
        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
        Instances For
          source
          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
          Instances For
            source
            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
            Instances For
              source
              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
              Instances For
                source
                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
                Instances For