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
    Instances For
      source
      @[reducible, inline]
      abbrev Lean.Meta.Grind.Arith.CommRing.NonCommSemiringM.run {α : Type} (semiringId : Nat) (x : NonCommSemiringM α) :
      GoalM α
      Instances For
        source
        @[implicit_reducible]
        instance Lean.Meta.Grind.Arith.CommRing.instMonadCanonNonCommSemiringM :
        MonadCanon NonCommSemiringM
        source
        def Lean.Meta.Grind.Arith.CommRing.NonCommSemiringM.getSemiring :
        NonCommSemiringM Semiring
        Instances For
          source
          def Lean.Meta.Grind.Arith.CommRing.NonCommSemiringM.modifySemiring (f : Semiring → Semiring) :
          NonCommSemiringM Unit
          Instances For
            source
            @[implicit_reducible]
            instance Lean.Meta.Grind.Arith.CommRing.instMonadSemiringNonCommSemiringM :
            MonadSemiring NonCommSemiringM
            source
            def Lean.Meta.Grind.Arith.CommRing.getTermNonCommSemiringId? (e : Expr) :
            GoalM (Option Nat)
            Instances For
              source
              def Lean.Meta.Grind.Arith.CommRing.setTermNonCommSemiringId (e : Expr) :
              NonCommSemiringM Unit
              Instances For
                source
                @[implicit_reducible]
                instance Lean.Meta.Grind.Arith.CommRing.instMonadSetTermIdNonCommSemiringM :
                MonadSetTermId NonCommSemiringM