def Lean.Meta.Grind.Arith.CommRing.pp? (goal : Goal) (rings : Array Sym.Arith.CommRing) : MetaM (Option MessageData)

Prints the ring solver state of goal. rings are the Sym.Arith records of the run (see Result.rings).

Both arrays are indexed by the ring id assigned by Sym.Arith.classify?: the goal's state is written at that id (RingM.modifyCommRingState), and the Sym.Arith array only grows during a run, so rings is at least as long as s.rings and rings[i] is the record of s.rings[i].

Equations

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

def Lean.Meta.Grind.Arith.CommRing.addThresholdMessage (goal : Goal) (c : Grind.Config) (msgs : Array MessageData) : IO (Array MessageData)

Equations

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