def Lean.Meta.Grind.Arith.Cutsat.isInterpretedTerm (e : Expr) : Bool

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.getAssignment? (goal : Goal) (e : Expr) : MetaM (Option Rat)

Equations

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

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

Construct a model that satisfies all constraints in the cutsat model. It also assigns values to integer terms that have not been internalized by the cutsat model.

Remark: it uses rational numbers because cutsat may have failed to build an integer model.

Equations

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