@[reducible, inline]

abbrev Lean.Meta.Sym.Arith.RingExpr : Type

@[reducible, inline]

abbrev Lean.Meta.Sym.Arith.SemiringExpr : Type

structure Lean.Meta.Sym.Arith.Semiring : Type

Classification state for a type with a Semiring instance.

• id : Nat
• type : Expr
• u : Level

  Cached getDecLevel type

• semiringInst : Expr

  Semiring instance for type

• addFn? : Option Expr
• mulFn? : Option Expr
• powFn? : Option Expr
• natCastFn? : Option Expr

@[implicit_reducible]

instance Lean.Meta.Sym.Arith.instInhabitedSemiring : Inhabited Semiring

structure Lean.Meta.Sym.Arith.Ring : Type

Classification state for a type with a Ring instance.

• id : Nat
• type : Expr
• u : Level

  Cached getDecLevel type

• ringInst : Expr

  Ring instance for type

• semiringInst : Expr

  Semiring instance for type

• charInst? : Option (Expr × Nat)

  IsCharP instance for type if available.

• addFn? : Option Expr
• mulFn? : Option Expr
• subFn? : Option Expr
• negFn? : Option Expr
• powFn? : Option Expr
• intCastFn? : Option Expr
• natCastFn? : Option Expr
• one? : Option Expr

@[implicit_reducible]

instance Lean.Meta.Sym.Arith.instInhabitedRing : Inhabited Ring

structure Lean.Meta.Sym.Arith.CommRingextends Lean.Meta.Sym.Arith.Ring : Type

Classification state for a type with a CommRing instance.

• id : Nat
• type : Expr
• u : Level
• ringInst : Expr
• semiringInst : Expr
• charInst? : Option (Expr × Nat)
• addFn? : Option Expr
• mulFn? : Option Expr
• subFn? : Option Expr
• negFn? : Option Expr
• powFn? : Option Expr
• intCastFn? : Option Expr
• natCastFn? : Option Expr
• one? : Option Expr
• invFn? : Option Expr

  Inverse function if fieldInst? is some inst

• semiringId? : Option Nat

  If this is a OfSemiring.Q α ring, this field contains the semiringId for α.

• commSemiringInst : Expr

  CommSemiring instance for type

• commRingInst : Expr

  CommRing instance for type

• noZeroDivInst? : Option Expr

  NoNatZeroDivisors instance for type if available.

• fieldInst? : Option Expr

  Field instance for type if available.

@[implicit_reducible]

instance Lean.Meta.Sym.Arith.instInhabitedCommRing : Inhabited CommRing

structure Lean.Meta.Sym.Arith.CommSemiringextends Lean.Meta.Sym.Arith.Semiring : Type

Classification state for a type with a CommSemiring instance. Recall that CommSemiring types are normalized using the OfSemiring.Q envelope.

• id : Nat
• type : Expr
• u : Level
• semiringInst : Expr
• addFn? : Option Expr
• mulFn? : Option Expr
• powFn? : Option Expr
• natCastFn? : Option Expr
• ringId : Nat

  Id of the envelope ring OfSemiring.Q type

• commSemiringInst : Expr

  CommSemiring instance for type

• addRightCancelInst? : Option (Option Expr)

  AddRightCancel instance for type if available.

• toQFn? : Option Expr

@[implicit_reducible]

instance Lean.Meta.Sym.Arith.instInhabitedCommSemiring : Inhabited CommSemiring

inductive Lean.Meta.Sym.Arith.ClassifyResult : Type

Result of classifying a type's algebraic structure.

• commRing (id : Nat) : ClassifyResult
• nonCommRing (id : Nat) : ClassifyResult
• commSemiring (id : Nat) : ClassifyResult
• nonCommSemiring (id : Nat) : ClassifyResult
• none : ClassifyResult

  No algebraic structure found.

@[implicit_reducible]

instance Lean.Meta.Sym.Arith.instInhabitedClassifyResult : Inhabited ClassifyResult

structure Lean.Meta.Sym.Arith.State : Type

Arith type classification state, stored as a SymExtension.

• exp : Nat

  Exponent threshold for HPow evaluation.

• rings : Array CommRing

  Commutative rings.

• semirings : Array CommSemiring

  Commutative semirings.

• ncRings : Array Ring

  Non-commutative rings.

• ncSemirings : Array Semiring

  Non-commutative semirings.

• typeClassify : PHashMap ExprPtr ClassifyResult

  Mapping from types to their classification result. Caches failures as .none.

@[implicit_reducible]

instance Lean.Meta.Sym.Arith.instInhabitedState : Inhabited State

opaque Lean.Meta.Sym.Arith.arithExt : SymExtension State

def Lean.Meta.Sym.Arith.getArithState : SymM State

@[inline]

def Lean.Meta.Sym.Arith.modifyArithState (f : State → State) : SymM Unit

def Lean.Meta.Sym.Arith.getExpThreshold : SymM Nat

Get the exponent threshold.

def Lean.Meta.Sym.Arith.setExpThreshold (exp : Nat) : SymM Unit

Set the exponent threshold.

def Lean.Meta.Sym.Arith.withExpThreshold {α : Type} (exp : Nat) (k : SymM α) : SymM α

Run k with a temporary exponent threshold.