Documentation

Lean.Meta.Tactic.Grind.Arith.CommRing.MonadCanon

source
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.

Instances
    source
    @[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.
    source
    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.
    Instances For