Documentation

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

source
def Lean.Meta.Grind.Arith.Linear.get' :
GoalM State
Instances For
    source
    @[inline]
    def Lean.Meta.Grind.Arith.Linear.modify' (f : State → State) :
    GoalM Unit
    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
          @[instance_reducible, always_inline]
          instance Lean.Meta.Grind.Arith.Linear.instMonadGetStructOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadGetStruct m] :
          MonadGetStruct n
          source
          @[reducible, inline]
          abbrev Lean.Meta.Grind.Arith.Linear.LinearM (α : Type) :
          Type

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

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