source
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.

Instances For

source
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.

Instances For