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

Equations

• Lean.Meta.Grind.propagateOffset (Lean.Meta.Grind.PendingTheoryPropagation.eq lhs rhs) = Lean.Meta.Grind.Arith.Offset.processNewEq lhs rhs
• Lean.Meta.Grind.propagateOffset x✝ = pure ()

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

Equations

• Lean.Meta.Grind.propagateCutsat (Lean.Meta.Grind.PendingTheoryPropagation.eq lhs rhs) = Lean.Meta.Grind.Arith.Cutsat.processNewEq lhs rhs
• Lean.Meta.Grind.propagateCutsat (Lean.Meta.Grind.PendingTheoryPropagation.diseqs ps) = Lean.Meta.Grind.propagateCutsatDiseqs ps
• Lean.Meta.Grind.propagateCutsat Lean.Meta.Grind.PendingTheoryPropagation.none = pure ()

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

Equations

• Lean.Meta.Grind.propagateCommRing (Lean.Meta.Grind.PendingTheoryPropagation.eq lhs rhs) = Lean.Meta.Grind.Arith.CommRing.processNewEq lhs rhs
• Lean.Meta.Grind.propagateCommRing (Lean.Meta.Grind.PendingTheoryPropagation.diseqs ps) = Lean.Meta.Grind.propagateCommRingDiseqs ps
• Lean.Meta.Grind.propagateCommRing x✝ = pure ()

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.

Equations

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

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

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

Equations

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

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.

Equations

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

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

Adds a new hypothesis.

Equations

• Lean.Meta.Grind.addHypothesis fvarId generation = do let __do_lift ← liftM fvarId.getType Lean.Meta.Grind.add __do_lift (Lean.mkFVar fvarId) generation