Algebraic structure classification

Detects the strongest algebraic structure available for a type and caches the classification in Arith.State.typeClassify. 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.