inductive Lean.Meta.Grind.PendingTheoryPropagation : Type

Equalities or disequalities to be propagated to a theory solver after two equivalence classes have been merged.

Some solvers (e.g. cutsat) require the core data structures to satisfy their invariants. During the merge operations some of these invariants do not hold. Thus, we first record the facts that must be propagated in a PendingTheoryPropagation value, complete the merge, and only then perform the propagation.

We now use this workflow for all theory solvers, even when a particular solver does not rely on these invariants. This keeps the core solver-agnostic and lets us modify solvers without further adjustments.

• none : PendingTheoryPropagation

  Nothing to propagate.

• eq (lhs rhs : Expr) : PendingTheoryPropagation

  Propagate the equality lhs = rhs.

• diseqs (ps : ParentSet) : PendingTheoryPropagation

  Propagate the disequalities in ps.

def Lean.Meta.Grind.propagateOffset : PendingTheoryPropagation → GoalM Unit

def Lean.Meta.Grind.propagateCutsat : PendingTheoryPropagation → GoalM Unit

def Lean.Meta.Grind.propagateCommRing : PendingTheoryPropagation → GoalM Unit

def Lean.Meta.Grind.propagateBeta (lams fns : Array Expr) : GoalM Unit

Tries to apply beta-reductiong using the parent applications of the functions in fns with the lambda expressions in lams.

def Lean.Meta.Grind.addNewEq (lhs rhs proof : Expr) (generation : Nat) : GoalM Unit

Internalizes lhs and rhs, and then adds equality lhs = rhs.

def Lean.Meta.Grind.add (fact proof : Expr) (generation : Nat := 0) : GoalM Unit

Adds a new fact justified by the given proof and using the given generation.

def Lean.Meta.Grind.addHypothesis (fvarId : FVarId) (generation : Nat := 0) : GoalM Unit

Adds a new hypothesis.