instance
Lean.Meta.Linear.instDecidableLtVarInstLTVar
(a : Lean.Meta.Linear.Var)
(b : Lean.Meta.Linear.Var)
:
@[inline, reducible]
Instances For
@[inline, reducible]
abbrev
Lean.Meta.Linear.Assignment.get?
(a : Lean.Meta.Linear.Assignment)
(x : Lean.Meta.Linear.Var)
:
Instances For
@[inline, reducible]
Instances For
@[inline, reducible]
Instances For
@[inline, reducible]
Instances For
@[inline, reducible]
Instances For
@[inline, reducible]
Instances For
@[inline, reducible]
abbrev
Lean.Meta.Linear.Poly.get
(e : Lean.Meta.Linear.Poly)
(i : Fin (Lean.Meta.Linear.Poly.size e))
:
Instances For
Instances For
Instances For
def
Lean.Meta.Linear.Poly.add.go
(e₁ : Lean.Meta.Linear.Poly)
(e₂ : Lean.Meta.Linear.Poly)
(i₁ : Nat)
(i₂ : Nat)
(r : Array (Int × Lean.Meta.Linear.Var))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Meta.Linear.Poly.combine
(d₁ : Int)
(e₁ : Lean.Meta.Linear.Poly)
(d₂ : Int)
(e₂ : Lean.Meta.Linear.Poly)
:
Instances For
def
Lean.Meta.Linear.Poly.combine.go
(d₁ : Int)
(e₁ : Lean.Meta.Linear.Poly)
(d₂ : Int)
(e₂ : Lean.Meta.Linear.Poly)
(i₁ : Nat)
(i₂ : Nat)
(r : Array (Int × Lean.Meta.Linear.Var))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
- combine: Int → Lean.Meta.Linear.Justification → Int → Lean.Meta.Linear.Justification → Lean.Meta.Linear.Justification
- assumption: Lean.Meta.Linear.AssumptionId → Lean.Meta.Linear.Justification
Instances For
- eq: Lean.Meta.Linear.CnstrKind
- div: Lean.Meta.Linear.CnstrKind
- lt: Lean.Meta.Linear.CnstrKind
- le: Lean.Meta.Linear.CnstrKind
Instances For
- kind : Lean.Meta.Linear.CnstrKind
- lhs : Lean.Meta.Linear.Poly
- rhs : Int
Instances For
@[inline, reducible]
Instances For
def
Lean.Meta.Linear.Cnstr.getBound
(c : Lean.Meta.Linear.Cnstr)
(a : Lean.Meta.Linear.Assignment)
:
Instances For
Instances For
def
Lean.Meta.Linear.getBestBound?
(cs : Array Lean.Meta.Linear.Cnstr)
(a : Lean.Meta.Linear.Assignment)
(isLower : Bool)
(isInt : Bool)
:
Instances For
- unsat: Lean.Meta.Linear.Justification → Lean.Meta.Linear.Result
- unsupported: Lean.Meta.Linear.Result
- timeout: Lean.Meta.Linear.Result
- sat: Lean.Meta.Linear.Assignment → Lean.Meta.Linear.Result
Instances For
- lowers : Array (Array Lean.Meta.Linear.Cnstr)
- uppers : Array (Array Lean.Meta.Linear.Cnstr)
- assignment : Lean.Meta.Linear.Assignment
Instances For
@[inline, reducible]
Instances For
@[inline, reducible]
Instances For
@[inline, reducible]
Instances For
@[inline, reducible]
Instances For
@[inline, reducible]
Instances For
def
Lean.Meta.Linear.resolve
(s : Lean.Meta.Linear.State)
(cl : Lean.Meta.Linear.Cnstr)
(cu : Lean.Meta.Linear.Cnstr)
:
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Lean.Meta.Linear.solve 0 s = Lean.Meta.Linear.Result.timeout