Documentation
Lean
.
Meta
.
Tactic
.
LinearArith
.
Simp
Search
Google site search
Lean
.
Meta
.
Tactic
.
LinearArith
.
Simp
source
Imports
Init
Lean.Meta.Tactic.LinearArith.Basic
Lean.Meta.Tactic.LinearArith.Nat.Simp
Imported by
Lean
.
Meta
.
Linear
.
simp?
source
def
Lean
.
Meta
.
Linear
.
simp?
(e :
Lean.Expr
)
(parent? :
Option
Lean.Expr
)
:
Lean.MetaM
(
Option
(
Lean.Expr
×
Lean.Expr
)
)
Equations
One or more equations did not get rendered due to their size.
Instances For