Documentation
Lean
.
Meta
.
Tactic
.
Grind
.
Arith
.
Cutsat
.
Var
Search
return to top
source
Imports
Lean.Meta.IntInstTesters
Lean.Meta.Tactic.Grind.Simp
Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Imported by
Lean
.
Meta
.
Grind
.
Arith
.
Cutsat
.
mkVarImpl
Lean
.
Meta
.
Grind
.
Arith
.
Cutsat
.
isInt
Lean
.
Meta
.
Grind
.
Arith
.
Cutsat
.
isAdd?
Lean
.
Meta
.
Grind
.
Arith
.
Cutsat
.
isAdd
Lean
.
Meta
.
Grind
.
Arith
.
Cutsat
.
isMul?
Lean
.
Meta
.
Grind
.
Arith
.
Cutsat
.
isMul
Lean
.
Meta
.
Grind
.
Arith
.
Cutsat
.
addMonomial
Lean
.
Meta
.
Grind
.
Arith
.
Cutsat
.
toPoly
Lean
.
Meta
.
Grind
.
Arith
.
Cutsat
.
toPoly
.
go
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
source
partial def
Lean
.
Meta
.
Grind
.
Arith
.
Cutsat
.
toPoly
.
go
(
e
:
Expr
)
(
p
:
Poly
)
:
GoalM
Poly