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
    Instances For
      source
      @[reducible, inline]
      abbrev Lean.Meta.Grind.Arith.Linear.OfNatModuleM.run {α : Type} (natStructId : Nat) (x : OfNatModuleM α) :
      GoalM α
      Instances For
        source
        @[reducible, inline]
        abbrev Lean.Meta.Grind.Arith.Linear.getNatStructId :
        OfNatModuleM Nat
        Instances For
          source
          def Lean.Meta.Grind.Arith.Linear.getNatStruct :
          OfNatModuleM NatStruct
          Instances For
            source
            def Lean.Meta.Grind.Arith.Linear.OfNatModuleM.getStruct :
            OfNatModuleM Struct
            Instances For
              source
              @[implicit_reducible]
              instance Lean.Meta.Grind.Arith.Linear.instMonadGetStructOfNatModuleM :
              MonadGetStruct OfNatModuleM
              source
              @[inline]
              def Lean.Meta.Grind.Arith.Linear.modifyNatStruct (f : NatStruct → NatStruct) :
              OfNatModuleM Unit
              Instances For
                source
                def Lean.Meta.Grind.Arith.Linear.getTermNatStructId? (e : Expr) :
                GoalM (Option Nat)
                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.

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