HepLean Documentation
Lean
.
Meta
.
Tactic
.
LinearArith
.
Nat
.
Simp
Search
Google site search
return to top
source
Imports
Lean.Meta.Tactic.LinearArith.Nat.Basic
Imported by
Lean
.
Meta
.
Linear
.
Nat
.
withAbstractAtoms
Lean
.
Meta
.
Linear
.
Nat
.
simpCnstrPos?
Lean
.
Meta
.
Linear
.
Nat
.
simpCnstr?
Lean
.
Meta
.
Linear
.
Nat
.
simpExpr?
source
def
Lean
.
Meta
.
Linear
.
Nat
.
withAbstractAtoms
(atoms :
Array
Lean.Expr
)
(k :
Array
Lean.Expr
→
Lean.MetaM
(
Option
(
Lean.Expr
×
Lean.Expr
)
)
)
:
Lean.MetaM
(
Option
(
Lean.Expr
×
Lean.Expr
)
)
Equations
One or more equations did not get rendered due to their size.
Instances For
source
def
Lean
.
Meta
.
Linear
.
Nat
.
simpCnstrPos?
(e :
Lean.Expr
)
:
Lean.MetaM
(
Option
(
Lean.Expr
×
Lean.Expr
)
)
Equations
One or more equations did not get rendered due to their size.
Instances For
source
def
Lean
.
Meta
.
Linear
.
Nat
.
simpCnstr?
(e :
Lean.Expr
)
:
Lean.MetaM
(
Option
(
Lean.Expr
×
Lean.Expr
)
)
Equations
One or more equations did not get rendered due to their size.
Instances For
source
def
Lean
.
Meta
.
Linear
.
Nat
.
simpExpr?
(e :
Lean.Expr
)
:
Lean.MetaM
(
Option
(
Lean.Expr
×
Lean.Expr
)
)
Equations
One or more equations did not get rendered due to their size.
Instances For