def Lean.Meta.Grind.Arith.Linear.getAssignment? (s : Struct) (e : Expr) : Option Rat

Equations

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

def Lean.Meta.Grind.Arith.Linear.mkModel (goal : Goal) (structId : Nat) : MetaM (Array (Expr × Rat))

Construct a model that satisfies all constraints in the linarith model for the structure with id structId. It also assigns values to (integer) terms that have not been internalized by the linarith model.

Equations

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