Documentation

Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM

source
structure Lean.Meta.Grind.Arith.CommRing.NonCommRingM.Context :
Type
Instances For
    source
    @[reducible, inline]
    abbrev Lean.Meta.Grind.Arith.CommRing.NonCommRingM (α : Type) :
    Type

    We don't want to keep carrying the RingId around.

    Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Lean.Meta.Grind.Arith.CommRing.NonCommRingM.run {α : Type} (ringId : Nat) (x : NonCommRingM α) :
        GoalM α
        Equations
          Instances For
            source
            instance Lean.Meta.Grind.Arith.CommRing.instMonadCanonNonCommRingM :
            MonadCanon NonCommRingM
            Equations
              source
              def Lean.Meta.Grind.Arith.CommRing.NonCommRingM.getRing :
              NonCommRingM Ring
              Equations
                Instances For
                  source
                  def Lean.Meta.Grind.Arith.CommRing.NonCommRingM.modifyRing (f : Ring → Ring) :
                  NonCommRingM Unit
                  Equations
                    Instances For
                      source
                      instance Lean.Meta.Grind.Arith.CommRing.instMonadRingNonCommRingM :
                      MonadRing NonCommRingM
                      Equations
                        source
                        def Lean.Meta.Grind.Arith.CommRing.getTermNonCommRingId? (e : Expr) :
                        GoalM (Option Nat)
                        Equations
                          Instances For
                            source
                            def Lean.Meta.Grind.Arith.CommRing.setTermNonCommRingId (e : Expr) :
                            NonCommRingM Unit
                            Equations
                              Instances For
                                source
                                instance Lean.Meta.Grind.Arith.CommRing.instMonadSetTermIdNonCommRingM :
                                MonadSetTermId NonCommRingM
                                Equations