Documentation

Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt

source
def Lean.Meta.Grind.Arith.Cutsat.getToIntInfo? (type : Expr) :
GoalM (Option ToIntInfo)
Equations
    Instances For
      source
      def Lean.Meta.Grind.Arith.Cutsat.getToIntInfo?.toIntInterval? (type rangeExpr : Expr) :
      GoalM (Option Grind.IntInterval)
      Equations
        Instances For
          source
          def Lean.Meta.Grind.Arith.Cutsat.getToIntInfo?.go? (type : Expr) :
          GoalM (Option ToIntInfo)
          Equations
            Instances For
              source
              structure Lean.Meta.Grind.Arith.Cutsat.ToIntM.Context :
              Type
              Instances For
                source
                @[reducible, inline]
                abbrev Lean.Meta.Grind.Arith.Cutsat.ToIntM (α : Type) :
                Type
                Equations
                  Instances For
                    source
                    def Lean.Meta.Grind.Arith.Cutsat.getInfo :
                    ToIntM ToIntInfo
                    Equations
                      Instances For
                        source
                        def Lean.Meta.Grind.Arith.Cutsat.ToIntM.run? {α : Type} (type : Expr) (x : ToIntM α) :
                        GoalM (Option α)
                        Equations
                          Instances For
                            source
                            def Lean.Meta.Grind.Arith.Cutsat.ToIntM.run (type : Expr) (x : ToIntM Unit) :
                            GoalM Unit
                            Equations
                              Instances For
                                source
                                def Lean.Meta.Grind.Arith.Cutsat.mkToIntVar (e : Expr) :
                                ToIntM (Expr × Expr)
                                Equations
                                  Instances For
                                    source
                                    def Lean.Meta.Grind.Arith.Cutsat.getToIntTermType? (e : Expr) :
                                    GoalM (Option Expr)
                                    Equations
                                      Instances For
                                        source
                                        def Lean.Meta.Grind.Arith.Cutsat.isToIntTerm (e : Expr) :
                                        GoalM Bool
                                        Equations
                                          Instances For
                                            source
                                            def Lean.Meta.Grind.Arith.Cutsat.toInt (a : Expr) :
                                            ToIntM (Expr × Expr)
                                            Equations
                                              Instances For
                                                source
                                                def Lean.Meta.Grind.Arith.Cutsat.toInt? (a type : Expr) :
                                                GoalM (Option (Expr × Expr))
                                                Equations
                                                  Instances For
                                                    source
                                                    def Lean.Meta.Grind.Arith.Cutsat.isSupportedType (type : Expr) :
                                                    GoalM Bool
                                                    Equations
                                                      Instances For
                                                        source
                                                        def Lean.Meta.Grind.Arith.Cutsat.assertToIntBounds (e : Expr) (x : Var) :
                                                        GoalM Unit

                                                        Given x whose denotation is e, if e is of the form ToInt a, asserts its lower and upper bounds if available

                                                        Equations
                                                          Instances For