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
    Instances For
      source
      @[reducible, inline]
      abbrev Lean.Meta.Grind.Arith.CommRing.SemiringM.run {α : Type} (semiringId : Nat) (x : SemiringM α) :
      GoalM α
      Instances For
        source
        @[reducible, inline]
        abbrev Lean.Meta.Grind.Arith.CommRing.getSemiringId :
        SemiringM Nat
        Instances For
          source
          @[implicit_reducible]
          instance Lean.Meta.Grind.Arith.CommRing.instMonadCanonSemiringM :
          MonadCanon SemiringM
          source
          def Lean.Meta.Grind.Arith.CommRing.SemiringM.getCommSemiring :
          SemiringM CommSemiring
          Instances For
            source
            @[inline]
            def Lean.Meta.Grind.Arith.CommRing.SemiringM.modifyCommSemiring (f : CommSemiring → CommSemiring) :
            SemiringM Unit
            Instances For
              source
              @[implicit_reducible]
              instance Lean.Meta.Grind.Arith.CommRing.instMonadCommSemiringSemiringM :
              MonadCommSemiring SemiringM
              source
              def Lean.Meta.Grind.Arith.CommRing.SemiringM.getCommRing :
              SemiringM CommRing
              Instances For
                source
                def Lean.Meta.Grind.Arith.CommRing.SemiringM.modifyCommRing (f : CommRing → CommRing) :
                SemiringM Unit
                Instances For
                  source
                  @[implicit_reducible]
                  instance Lean.Meta.Grind.Arith.CommRing.instMonadCommRingSemiringM :
                  MonadCommRing SemiringM
                  source
                  def Lean.Meta.Grind.Arith.CommRing.getToQFn :
                  SemiringM Expr
                  Instances For
                    source
                    def Lean.Meta.Grind.Arith.CommRing.getAddRightCancelInst? :
                    SemiringM (Option Expr)
                    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
                      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
                        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
                          Instances For
                            source
                            def Lean.Meta.Grind.Arith.CommRing.getNatCastFn' {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadSemiring m] :
                            m Expr
                            Instances For
                              source
                              def Lean.Meta.Grind.Arith.CommRing.getTermSemiringId? (e : Expr) :
                              GoalM (Option Nat)
                              Instances For
                                source
                                def Lean.Meta.Grind.Arith.CommRing.setTermSemiringId (e : Expr) :
                                SemiringM Unit
                                Instances For
                                  source
                                  @[implicit_reducible]
                                  instance Lean.Meta.Grind.Arith.CommRing.instMonadSetTermIdSemiringM :
                                  MonadSetTermId SemiringM
                                  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

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