Algebraic structure classification

Detects the strongest algebraic structure available for a type and caches the classification in Arith.State.typeClassify. The state is a SymExtension, so a type is classified once per SymM run and the result is shared by every grind goal and every tactic of a sym block. The detection order is:

1. Grind.CommRing (includes Field check)
2. Grind.Ring (non-commutative)
3. Grind.CommSemiring (via OfSemiring.Q envelope)
4. Grind.Semiring (non-commutative)

Results (including failures) are cached in a single PHashMap ExprPtr ClassifyResult to avoid repeated synthesis attempts.

def Lean.Meta.Sym.Arith.classify? (type : Expr) : SymM ClassifyResult

Classify the algebraic structure of type, trying the strongest first: CommRing > Ring > CommSemiring > Semiring. Results are cached in Arith.State.typeClassify.

Equations

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

def Lean.Meta.Sym.Arith.classifyOrder? (type : Expr) : SymM (Option Nat)

Classify type as an order structure (at least IsPreorder), returning its id in State.orders. Results, including failures, are cached in State.typeOrderClassify.

Equations

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