Documentation
Lean.Meta.Tactic.LinearArith.Simp
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.