Documentation

Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM

source
structure Lean.Meta.Grind.Arith.CommRing.NonCommSemiringM.Context :
Type
  • semiringId : Nat
Instances For
    source
    @[reducible, inline]
    abbrev Lean.Meta.Grind.Arith.CommRing.NonCommSemiringM (α : Type) :
    Type
    Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Lean.Meta.Grind.Arith.CommRing.NonCommSemiringM.run {α : Type} (semiringId : Nat) (x : NonCommSemiringM α) :
        GoalM α
        Equations
          Instances For
            source
            instance Lean.Meta.Grind.Arith.CommRing.instMonadCanonNonCommSemiringM :
            MonadCanon NonCommSemiringM
            Equations
              source
              def Lean.Meta.Grind.Arith.CommRing.NonCommSemiringM.getSemiring :
              NonCommSemiringM Semiring
              Equations
                Instances For
                  source
                  def Lean.Meta.Grind.Arith.CommRing.NonCommSemiringM.modifySemiring (f : Semiring → Semiring) :
                  NonCommSemiringM Unit
                  Equations
                    Instances For
                      source
                      instance Lean.Meta.Grind.Arith.CommRing.instMonadSemiringNonCommSemiringM :
                      MonadSemiring NonCommSemiringM
                      Equations
                        source
                        def Lean.Meta.Grind.Arith.CommRing.getTermNonCommSemiringId? (e : Expr) :
                        GoalM (Option Nat)
                        Equations
                          Instances For
                            source
                            def Lean.Meta.Grind.Arith.CommRing.setTermNonCommSemiringId (e : Expr) :
                            NonCommSemiringM Unit
                            Equations
                              Instances For
                                source
                                instance Lean.Meta.Grind.Arith.CommRing.instMonadSetTermIdNonCommSemiringM :
                                MonadSetTermId NonCommSemiringM
                                Equations