Documentation
Lean
.
Meta
.
Tactic
.
Simp
.
Arith
.
Int
.
Simp
Search
return to top
source
Imports
Lean.Meta.Tactic.Simp.Arith.Util
Lean.Meta.Tactic.Simp.Arith.Int.Basic
Imported by
Int
.
Linear
.
Poly
.
gcdAll
Int
.
Linear
.
Poly
.
gcdAll
.
go
Int
.
Linear
.
Poly
.
gcdCoeffs'
Int
.
Linear
.
Poly
.
gcdCoeffs'
.
go
Lean
.
Meta
.
Simp
.
Arith
.
Int
.
simpEq?
Lean
.
Meta
.
Simp
.
Arith
.
Int
.
simpLe?
Lean
.
Meta
.
Simp
.
Arith
.
Int
.
simpRel?
Lean
.
Meta
.
Simp
.
Arith
.
Int
.
simpDvd?
Lean
.
Meta
.
Simp
.
Arith
.
Int
.
simpExpr?
source
def
Int
.
Linear
.
Poly
.
gcdAll
:
Poly
→
Nat
Equations
Instances For
source
def
Int
.
Linear
.
Poly
.
gcdAll
.
go
(
k
:
Nat
)
(
p
:
Poly
)
:
Nat
Equations
Instances For
source
def
Int
.
Linear
.
Poly
.
gcdCoeffs'
:
Poly
→
Nat
Equations
Instances For
source
def
Int
.
Linear
.
Poly
.
gcdCoeffs'
.
go
(
k
:
Nat
)
(
p
:
Poly
)
:
Nat
Equations
Instances For
source
def
Lean
.
Meta
.
Simp
.
Arith
.
Int
.
simpEq?
(
e
:
Expr
)
:
MetaM
(
Option
(
Expr
×
Expr
))
Equations
Instances For
source
def
Lean
.
Meta
.
Simp
.
Arith
.
Int
.
simpLe?
(
e
:
Expr
)
(
checkIfModified
:
Bool
)
:
MetaM
(
Option
(
Expr
×
Expr
))
Equations
Instances For
source
def
Lean
.
Meta
.
Simp
.
Arith
.
Int
.
simpRel?
(
e
:
Expr
)
:
MetaM
(
Option
(
Expr
×
Expr
))
Equations
Instances For
source
def
Lean
.
Meta
.
Simp
.
Arith
.
Int
.
simpDvd?
(
e
:
Expr
)
:
MetaM
(
Option
(
Expr
×
Expr
))
Equations
Instances For
source
def
Lean
.
Meta
.
Simp
.
Arith
.
Int
.
simpExpr?
(
lhs
:
Expr
)
:
MetaM
(
Option
(
Expr
×
Expr
))
Equations
Instances For