def Lean.Meta.Grind.Arith.Cutsat.embeddingArg? (e : Expr) : Option Expr

If e is a single embedding step — an accessor application (Fin.val a, BitVec.toNat a, BitVec.toInt a) or a conversion to BitVec (a.toBitVec) — returns a. The value of e determines the value of a. Unlike isEmbeddingApp?, chains such as a.toBitVec.toNat are not collapsed; callers resolve them one step at a time.

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

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.