Documentation

Lean.Meta.Tactic.Grind.Arith.Linear.Reify

source
def Lean.Meta.Grind.Arith.Linear.isAddInst (struct : Struct) (inst : Expr) :
Bool
Instances For
    source
    def Lean.Meta.Grind.Arith.Linear.isZeroInst (struct : Struct) (inst : Expr) :
    Bool
    Instances For
      source
      def Lean.Meta.Grind.Arith.Linear.isSMulIntInst (struct : Struct) (inst : Expr) :
      Bool
      Instances For
        source
        def Lean.Meta.Grind.Arith.Linear.isSMulNatInst (struct : Struct) (inst : Expr) :
        Bool
        Instances For
          source
          def Lean.Meta.Grind.Arith.Linear.isHomoMulInst (struct : Struct) (inst : Expr) :
          Bool
          Instances For
            source
            def Lean.Meta.Grind.Arith.Linear.isHSMulIntInst (struct : Struct) (inst : Expr) :
            Bool
            Instances For
              source
              def Lean.Meta.Grind.Arith.Linear.isHSMulNatInst (struct : Struct) (inst : Expr) :
              Bool
              Instances For
                source
                def Lean.Meta.Grind.Arith.Linear.isSubInst (struct : Struct) (inst : Expr) :
                Bool
                Instances For
                  source
                  def Lean.Meta.Grind.Arith.Linear.isNegInst (struct : Struct) (inst : Expr) :
                  Bool
                  Instances For
                    source
                    def Lean.Meta.Grind.Arith.Linear.reportInstIssue (e : Expr) :
                    GoalM Unit
                    Instances For
                      source
                      def Lean.Meta.Grind.Arith.Linear.reify? (e : Expr) (skipVar : Bool) :
                      LinearM (Option LinExpr)

                      Converts a Lean IntModule expression e into a LinExpr

                      If skipVar is true, then the result is none if e is not an interpreted IntModule term. We use skipVar := false when processing inequalities, and skipVar := true for equalities and disequalities

                      Instances For