Documentation

Lean.Meta.Tactic.Grind.Arith.Linear.OfNatModule

source
structure Lean.Meta.Grind.Arith.Linear.OfNatModuleM.Context :
Type
  • natStructId : Nat
Instances For
    source
    @[reducible, inline]
    abbrev Lean.Meta.Grind.Arith.Linear.OfNatModuleM (α : Type) :
    Type
    Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Lean.Meta.Grind.Arith.Linear.OfNatModuleM.run {α : Type} (natStructId : Nat) (x : OfNatModuleM α) :
        GoalM α
        Equations
          Instances For
            source
            @[reducible, inline]
            abbrev Lean.Meta.Grind.Arith.Linear.getNatStructId :
            OfNatModuleM Nat
            Equations
              Instances For
                source
                def Lean.Meta.Grind.Arith.Linear.getNatStruct :
                OfNatModuleM NatStruct
                Equations
                  Instances For
                    source
                    def Lean.Meta.Grind.Arith.Linear.OfNatModuleM.getStruct :
                    OfNatModuleM Struct
                    Equations
                      Instances For
                        source
                        instance Lean.Meta.Grind.Arith.Linear.instMonadGetStructOfNatModuleM :
                        MonadGetStruct OfNatModuleM
                        Equations
                          source
                          @[inline]
                          def Lean.Meta.Grind.Arith.Linear.modifyNatStruct (f : NatStruct → NatStruct) :
                          OfNatModuleM Unit
                          Equations
                            Instances For
                              source
                              def Lean.Meta.Grind.Arith.Linear.getTermNatStructId? (e : Expr) :
                              GoalM (Option Nat)
                              Equations
                                Instances For
                                  source
                                  def Lean.Meta.Grind.Arith.Linear.inSameNatStruct? (a b : Expr) :
                                  GoalM (Option Nat)

                                  Returns some natStructId if a and b are elements of the same NatModule structure.

                                  Equations
                                    Instances For
                                      source
                                      def Lean.Meta.Grind.Arith.Linear.setTermNatStructId (e : Expr) :
                                      OfNatModuleM Unit
                                      Equations
                                        Instances For
                                          source
                                          def Lean.Meta.Grind.Arith.Linear.ofNatModule (e : Expr) :
                                          OfNatModuleM (Expr × Expr)
                                          Equations
                                            Instances For
                                              source
                                              def Lean.Meta.Grind.Arith.Linear.normNatModuleDiseq (a b : Expr) :
                                              OfNatModuleM Unit
                                              Equations
                                                Instances For