Documentation

Lean.Meta.Tactic.Grind.Arith.Cutsat.Var

source
@[extern lean_cutsat_propagate_nonlinear]
opaque Lean.Meta.Grind.Arith.Cutsat.propagateNonlinearTerm (y x : Var) :
GoalM Bool
source
@[export lean_grind_cutsat_mk_var]
def Lean.Meta.Grind.Arith.Cutsat.mkVarImpl (expr : Expr) :
GoalM Var
Equations
    Instances For
      source
      def Lean.Meta.Grind.Arith.Cutsat.isInt (e : Expr) :
      GoalM Bool
      Equations
        Instances For
          source
          def Lean.Meta.Grind.Arith.Cutsat.isAdd? (e : Expr) (report : Bool := true) :
          GoalM (Option (Expr × Expr))
          Equations
            Instances For
              source
              def Lean.Meta.Grind.Arith.Cutsat.isAdd (e : Expr) :
              GoalM Bool
              Equations
                Instances For
                  source
                  def Lean.Meta.Grind.Arith.Cutsat.isMul? (e : Expr) (report : Bool := true) :
                  GoalM (Option (Int × Expr))
                  Equations
                    Instances For
                      source
                      def Lean.Meta.Grind.Arith.Cutsat.isMul (e : Expr) :
                      GoalM Bool
                      Equations
                        Instances For
                          source
                          def Lean.Meta.Grind.Arith.Cutsat.addMonomial (e : Expr) (p : Poly) :
                          GoalM Poly
                          Equations
                            Instances For
                              source
                              def Lean.Meta.Grind.Arith.Cutsat.toPoly (e : Expr) :
                              GoalM Poly
                              Equations
                                Instances For