structure Lean.Meta.Grind.Arith.Linear.Case : Type

• c : DiseqCnstr
• fvarId : FVarId

  Decision variable used to represent the case-split. For example, suppose we are splitting on p ≠ 0. Then, we create a decision variable h : p < 0

• saved : Struct

  Snapshot of the state for backtracking purposes. We do not use a trail stack.

def Lean.Meta.Grind.Arith.Linear.instInhabitedCase.default : Case

Equations

• Lean.Meta.Grind.Arith.Linear.instInhabitedCase.default = { c := default, fvarId := default, saved := default }

instance Lean.Meta.Grind.Arith.Linear.instInhabitedCase : Inhabited Case

Equations

• Lean.Meta.Grind.Arith.Linear.instInhabitedCase = { default := Lean.Meta.Grind.Arith.Linear.instInhabitedCase.default }

structure Lean.Meta.Grind.Arith.Linear.Search.State : Type

State of the model search procedure.

• cases : PArray Case

  Decision stack (aka case-split stack)

• decVars : FVarIdSet

  Set of decision variables in cases.

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Linear.SearchM (α : Type) : Type

Equations

• Lean.Meta.Grind.Arith.Linear.SearchM = StateRefT' IO.RealWorld Lean.Meta.Grind.Arith.Linear.Search.State Lean.Meta.Grind.Arith.Linear.LinearM

def Lean.Meta.Grind.Arith.Linear.mkCase (c : DiseqCnstr) : SearchM FVarId

Equations

• One or more equations did not get rendered due to their size.