Documentation

Lean.Meta.Tactic.Grind.Arith.Cutsat.Model

Equations
    Instances For

      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
        Instances For