Equations
- Lean.Meta.Linear.instInhabitedVar = { default := { id := default } }
Equations
- Lean.Meta.Linear.instOrdVar = { compare := Lean.Meta.Linear.ordVar✝ }
Equations
- Lean.Meta.Linear.instReprVar = { reprPrec := Lean.Meta.Linear.reprVar✝ }
Equations
- Lean.Meta.Linear.instLTVar = { lt := fun a b => a.id < b.id }
instance
Lean.Meta.Linear.instDecidableLtVarInstLTVar
(a : Lean.Meta.Linear.Var)
(b : Lean.Meta.Linear.Var)
:
Equations
- Lean.Meta.Linear.instDecidableLtVarInstLTVar a b = inferInstanceAs (Decidable (a.id < b.id))
Equations
- Lean.Meta.Linear.instInhabitedAssignment = { default := { val := default } }
@[inline, reducible]
Equations
Instances For
@[inline, reducible]
abbrev
Lean.Meta.Linear.Assignment.get?
(a : Lean.Meta.Linear.Assignment)
(x : Lean.Meta.Linear.Var)
:
Equations
- Lean.Meta.Linear.Assignment.get? a x = if h : x.id < Lean.Meta.Linear.Assignment.size a then some (Array.get a.val { val := x.id, isLt := h }) else none
Instances For
@[inline, reducible]
Equations
- Lean.Meta.Linear.Assignment.push a v = { val := Array.push a.val v }
Instances For
@[inline, reducible]
Equations
- Lean.Meta.Linear.Assignment.shrink a newSize = { val := Array.shrink a.val newSize }
Instances For
Equations
- Lean.Meta.Linear.instInhabitedPoly = { default := { val := default } }
Equations
- Lean.Meta.Linear.instReprPoly = { reprPrec := Lean.Meta.Linear.reprPoly✝ }
@[inline, reducible]
Equations
- Lean.Meta.Linear.Poly.getMaxVarCoeff e = (Array.back e.val).fst
Instances For
@[inline, reducible]
Equations
- Lean.Meta.Linear.Poly.getMaxVar e = (Array.back e.val).snd
Instances For
@[inline, reducible]
abbrev
Lean.Meta.Linear.Poly.get
(e : Lean.Meta.Linear.Poly)
(i : Fin (Lean.Meta.Linear.Poly.size e))
:
Equations
- Lean.Meta.Linear.Poly.get e i = Array.get e.val i
Instances For
Equations
- Lean.Meta.Linear.Poly.scale d e = { val := Array.map (fun x => match x with | (c, x) => (c * d, x)) e.val }
Instances For
Equations
- Lean.Meta.Linear.Poly.add e₁ e₂ = Lean.Meta.Linear.Poly.add.go e₁ e₂ 0 0 #[]
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)
:
Equations
- Lean.Meta.Linear.Poly.combine d₁ e₁ d₂ e₂ = Lean.Meta.Linear.Poly.combine.go d₁ e₁ d₂ e₂ 0 0 #[]
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.Linear.instInhabitedAssumptionId = { default := { id := default } }
Equations
- Lean.Meta.Linear.instReprAssumptionId = { reprPrec := Lean.Meta.Linear.reprAssumptionId✝ }
- 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
Equations
- Lean.Meta.Linear.instInhabitedJustification = { default := Lean.Meta.Linear.Justification.assumption default }
Equations
- eq: Lean.Meta.Linear.CnstrKind
- div: Lean.Meta.Linear.CnstrKind
- lt: Lean.Meta.Linear.CnstrKind
- le: Lean.Meta.Linear.CnstrKind
Instances For
Equations
Equations
- Lean.Meta.Linear.instDecidableEqCnstrKind x y = if h : Lean.Meta.Linear.CnstrKind.toCtorIdx x = Lean.Meta.Linear.CnstrKind.toCtorIdx y then isTrue (_ : x = y) else isFalse (_ : x = y → False)
Equations
Equations
- Lean.Meta.Linear.instReprCnstrKind = { reprPrec := Lean.Meta.Linear.reprCnstrKind✝ }
- kind : Lean.Meta.Linear.CnstrKind
- lhs : Lean.Meta.Linear.Poly
- rhs : Int
Instances For
Equations
- Lean.Meta.Linear.instInhabitedCnstr = { default := { kind := default, lhs := default, rhs := default, jst := default } }
Equations
Equations
- Lean.Meta.Linear.instReprCnstr = { reprPrec := Lean.Meta.Linear.reprCnstr✝ }
@[inline, reducible]
Equations
- Lean.Meta.Linear.Cnstr.isStrict c = match c.kind with | Lean.Meta.Linear.CnstrKind.lt => true | x => false
Instances For
def
Lean.Meta.Linear.Cnstr.getBound
(c : Lean.Meta.Linear.Cnstr)
(a : Lean.Meta.Linear.Assignment)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Meta.Linear.getBestBound?
(cs : Array Lean.Meta.Linear.Cnstr)
(a : Lean.Meta.Linear.Assignment)
(isLower : Bool)
(isInt : Bool)
:
Equations
- One or more equations did not get rendered due to their size.
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
Equations
- Lean.Meta.Linear.instInhabitedState = { default := { lowers := default, uppers := default, int := default, assignment := default } }
@[inline, reducible]
Equations
- Lean.Meta.Linear.State.getNumVars s = Array.size s.lowers
Instances For
@[inline, reducible]
Equations
- Lean.Meta.Linear.State.currVar s = Lean.Meta.Linear.Assignment.size s.assignment
Instances For
@[inline, reducible]
Equations
- Lean.Meta.Linear.State.getBestLowerBound? s = Lean.Meta.Linear.getBestBound? s.lowers[Lean.Meta.Linear.State.currVar s]! s.assignment true s.int[Lean.Meta.Linear.State.currVar s]!
Instances For
@[inline, reducible]
Equations
- Lean.Meta.Linear.State.getBestUpperBound? s = Lean.Meta.Linear.getBestBound? s.uppers[Lean.Meta.Linear.State.currVar s]! s.assignment false s.int[Lean.Meta.Linear.State.currVar s]!
Instances For
@[inline, reducible]
Equations
- Lean.Meta.Linear.State.assignCurr s v = { lowers := s.lowers, uppers := s.uppers, int := s.int, assignment := Lean.Meta.Linear.Assignment.push s.assignment v }
Instances For
def
Lean.Meta.Linear.resolve
(s : Lean.Meta.Linear.State)
(cl : Lean.Meta.Linear.Cnstr)
(cu : Lean.Meta.Linear.Cnstr)
:
Equations
- One or more equations did not get rendered due to their size.
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