Documentation

Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM

source
structure Lean.Meta.Grind.Arith.CommRing.SemiringM.Context :
Type
  • semiringId : Nat
Instances For
    source
    @[reducible, inline]
    abbrev Lean.Meta.Grind.Arith.CommRing.SemiringM (α : Type) :
    Type
    Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Lean.Meta.Grind.Arith.CommRing.SemiringM.run {α : Type} (semiringId : Nat) (x : SemiringM α) :
        GoalM α
        Equations
          Instances For
            source
            @[reducible, inline]
            abbrev Lean.Meta.Grind.Arith.CommRing.getSemiringId :
            SemiringM Nat
            Equations
              Instances For
                source
                instance Lean.Meta.Grind.Arith.CommRing.instMonadCanonSemiringM :
                MonadCanon SemiringM
                Equations
                  source
                  def Lean.Meta.Grind.Arith.CommRing.SemiringM.getCommSemiring :
                  SemiringM CommSemiring
                  Equations
                    Instances For
                      source
                      @[inline]
                      def Lean.Meta.Grind.Arith.CommRing.SemiringM.modifyCommSemiring (f : CommSemiring → CommSemiring) :
                      SemiringM Unit
                      Equations
                        Instances For
                          source
                          instance Lean.Meta.Grind.Arith.CommRing.instMonadCommSemiringSemiringM :
                          MonadCommSemiring SemiringM
                          Equations
                            source
                            def Lean.Meta.Grind.Arith.CommRing.SemiringM.getCommRing :
                            SemiringM CommRing
                            Equations
                              Instances For
                                source
                                def Lean.Meta.Grind.Arith.CommRing.SemiringM.modifyCommRing (f : CommRing → CommRing) :
                                SemiringM Unit
                                Equations
                                  Instances For
                                    source
                                    instance Lean.Meta.Grind.Arith.CommRing.instMonadCommRingSemiringM :
                                    MonadCommRing SemiringM
                                    Equations
                                      source
                                      def Lean.Meta.Grind.Arith.CommRing.getToQFn :
                                      SemiringM Expr
                                      Equations
                                        Instances For
                                          source
                                          def Lean.Meta.Grind.Arith.CommRing.getAddRightCancelInst? :
                                          SemiringM (Option Expr)
                                          Equations
                                            Instances For
                                              source
                                              def Lean.Meta.Grind.Arith.CommRing.getAddFn' {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] :
                                              m Expr
                                              Equations
                                                Instances For
                                                  source
                                                  def Lean.Meta.Grind.Arith.CommRing.getMulFn' {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] :
                                                  m Expr
                                                  Equations
                                                    Instances For
                                                      source
                                                      def Lean.Meta.Grind.Arith.CommRing.getPowFn' {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] :
                                                      m Expr
                                                      Equations
                                                        Instances For
                                                          source
                                                          def Lean.Meta.Grind.Arith.CommRing.getNatCastFn' {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadSemiring m] :
                                                          m Expr
                                                          Equations
                                                            Instances For
                                                              source
                                                              def Lean.Meta.Grind.Arith.CommRing.getTermSemiringId? (e : Expr) :
                                                              GoalM (Option Nat)
                                                              Equations
                                                                Instances For
                                                                  source
                                                                  def Lean.Meta.Grind.Arith.CommRing.setTermSemiringId (e : Expr) :
                                                                  SemiringM Unit
                                                                  Equations
                                                                    Instances For
                                                                      source
                                                                      instance Lean.Meta.Grind.Arith.CommRing.instMonadSetTermIdSemiringM :
                                                                      MonadSetTermId SemiringM
                                                                      Equations
                                                                        source
                                                                        def Lean.Meta.Grind.Arith.CommRing.mkSVarCore {m : Type → Type} [MonadLiftT GoalM m] [Monad m] [MonadSemiring m] [MonadSetTermId m] (e : Expr) :
                                                                        m Var

                                                                        Similar to mkVarCore but for Semirings

                                                                        Equations
                                                                          Instances For
                                                                            source
                                                                            def Lean.Meta.Grind.Arith.CommRing.mkSVar (e : Expr) :
                                                                            SemiringM Var
                                                                            Equations
                                                                              Instances For
                                                                                source
                                                                                def Lean.Grind.CommRing.Expr.denoteAsRingExpr (e : Meta.Grind.Arith.CommRing.SemiringExpr) :
                                                                                Meta.Grind.Arith.CommRing.SemiringM Lean.Expr
                                                                                Equations
                                                                                  Instances For