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
Instances For
    source
    def Lean.Meta.Grind.Arith.Cutsat.isInt (e : Expr) :
    GoalM Bool
    Instances For
      source
      def Lean.Meta.Grind.Arith.Cutsat.isAdd? (e : Expr) (report : Bool := true) :
      GoalM (Option (Expr × Expr))
      Instances For
        source
        def Lean.Meta.Grind.Arith.Cutsat.isAdd (e : Expr) :
        GoalM Bool
        Instances For
          source
          def Lean.Meta.Grind.Arith.Cutsat.isMul? (e : Expr) (report : Bool := true) :
          GoalM (Option (Int × Expr))
          Instances For
            source
            def Lean.Meta.Grind.Arith.Cutsat.isMul (e : Expr) :
            GoalM Bool
            Instances For
              source
              def Lean.Meta.Grind.Arith.Cutsat.addMonomial (e : Expr) (p : Poly) :
              GoalM Poly
              Instances For
                source
                def Lean.Meta.Grind.Arith.Cutsat.toPoly (e : Expr) :
                GoalM Poly
                Instances For