Documentation
Lean
.
Meta
.
Tactic
.
LinearArith
.
Nat
.
Solver
Search
Google site search
return to top
source
Imports
Init
Lean.Meta.Tactic.LinearArith.Solver
Lean.Meta.Tactic.LinearArith.Nat.Basic
Imported by
Lean
.
Meta
.
Linear
.
Nat
.
Collect
.
LinearArith
Lean
.
Meta
.
Linear
.
Nat
.
Collect
.
Cnstr
Lean
.
Meta
.
Linear
.
Nat
.
Collect
.
State
Lean
.
Meta
.
Linear
.
Nat
.
Collect
.
M
source
inductive
Lean
.
Meta
.
Linear
.
Nat
.
Collect
.
LinearArith
:
Type
Instances For
source
structure
Lean
.
Meta
.
Linear
.
Nat
.
Collect
.
Cnstr
:
Type
cnstr :
Lean.Meta.Linear.Nat.Collect.LinearArith
proof :
Lean.Expr
Instances For
source
structure
Lean
.
Meta
.
Linear
.
Nat
.
Collect
.
State
:
Type
cnstrs :
Array
Lean.Meta.Linear.Nat.Collect.Cnstr
Instances For
source
@[inline, reducible]
abbrev
Lean
.
Meta
.
Linear
.
Nat
.
Collect
.
M
(α :
Type
)
:
Type
Equations
Lean.Meta.Linear.Nat.Collect.M
=
StateRefT'
IO.RealWorld
Lean.Meta.Linear.Nat.Collect.State
Lean.Meta.Linear.Nat.ToLinear.M
Instances For