Documentation

Lean.Meta.Tactic.Grind.Arith.Linear.LinearM

source
def Lean.Meta.Grind.Arith.Linear.get' :
GoalM State
Equations
    Instances For
      source
      @[inline]
      def Lean.Meta.Grind.Arith.Linear.modify' (f : State → State) :
      GoalM Unit
      Equations
        Instances For
          source
          structure Lean.Meta.Grind.Arith.Linear.LinearM.Context :
          Type
          Instances For
            source
            class Lean.Meta.Grind.Arith.Linear.MonadGetStruct (m : Type → Type) :
            Type
            Instances
              source
              @[always_inline]
              instance Lean.Meta.Grind.Arith.Linear.instMonadGetStructOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadGetStruct m] :
              MonadGetStruct n
              Equations
                source
                @[reducible, inline]
                abbrev Lean.Meta.Grind.Arith.Linear.LinearM (α : Type) :
                Type

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

                Equations
                  Instances For
                    source
                    @[reducible, inline]
                    abbrev Lean.Meta.Grind.Arith.Linear.LinearM.run {α : Type} (structId : Nat) (x : LinearM α) :
                    GoalM α
                    Equations
                      Instances For
                        source
                        @[reducible, inline]
                        abbrev Lean.Meta.Grind.Arith.Linear.getStructId :
                        LinearM Nat
                        Equations
                          Instances For
                            source
                            def Lean.Meta.Grind.Arith.Linear.LinearM.getStruct :
                            LinearM Struct
                            Equations
                              Instances For
                                source
                                instance Lean.Meta.Grind.Arith.Linear.instMonadGetStructLinearM :
                                MonadGetStruct LinearM
                                Equations
                                  source
                                  def Lean.Meta.Grind.Arith.Linear.getRingCore? (ringId? : Option Nat) :
                                  GoalM (Option CommRing.Ring)
                                  Equations
                                    Instances For
                                      source
                                      def Lean.Meta.Grind.Arith.Linear.throwNotRing {α : Type} :
                                      LinearM α
                                      Equations
                                        Instances For
                                          source
                                          def Lean.Meta.Grind.Arith.Linear.throwNotCommRing {α : Type} :
                                          LinearM α
                                          Equations
                                            Instances For
                                              source
                                              def Lean.Meta.Grind.Arith.Linear.getRing? :
                                              LinearM (Option CommRing.Ring)
                                              Equations
                                                Instances For
                                                  source
                                                  instance Lean.Meta.Grind.Arith.Linear.instMonadCanonLinearM :
                                                  CommRing.MonadCanon LinearM
                                                  Equations
                                                    source
                                                    def Lean.Meta.Grind.Arith.Linear.LinearM.getRing :
                                                    LinearM CommRing.Ring
                                                    Equations
                                                      Instances For
                                                        source
                                                        instance Lean.Meta.Grind.Arith.Linear.instMonadRingLinearM :
                                                        CommRing.MonadRing LinearM
                                                        Equations
                                                          source
                                                          def Lean.Meta.Grind.Arith.Linear.withRingM {α : Type} (x : CommRing.RingM α) :
                                                          LinearM α
                                                          Equations
                                                            Instances For
                                                              source
                                                              @[inline]
                                                              def Lean.Meta.Grind.Arith.Linear.modifyStruct (f : Struct → Struct) :
                                                              LinearM Unit
                                                              Equations
                                                                Instances For