class Lean.Meta.Grind.Arith.CommRing.MonadCanon (m : Type → Type) : Type

• canonExpr : Expr → m Expr

  Helper function for removing dependency on GoalM. In RingM and SemiringM, this is just sharedCommon (← canon e) When printing counterexamples, we are at MetaM, and this is just the identity function.

• synthInstance? : Expr → m (Option Expr)

  Helper function for removing dependency on GoalM. During search we want to track the instances synthesized by grind, and this is Grind.synthInstance.

@[always_inline]

instance Lean.Meta.Grind.Arith.CommRing.instMonadCanonOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadCanon m] : MonadCanon n

def Lean.Meta.Grind.Arith.CommRing.MonadCanon.synthInstance {m : Type → Type} [Monad m] [MonadError m] [MonadCanon m] (type : Expr) : m Expr