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

Equations

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

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

Equations

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

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

• getRing : m Ring
• modifyRing : (Ring → Ring) → m Unit

@[always_inline]

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

Equations

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

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

• getCommRing : m CommRing
• modifyCommRing : (CommRing → CommRing) → m Unit

@[always_inline]

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

Equations

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

@[always_inline]

instance Lean.Meta.Grind.Arith.CommRing.instMonadRingOfMonadOfMonadCommRing (m : Type → Type) [Monad m] [MonadCommRing m] : MonadRing m

Equations

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