@[reducible, inline]

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

Equations

• Lean.Meta.Sym.Arith.RingExpr = Lean.Grind.CommRing.Expr

@[reducible, inline]

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

Equations

• Lean.Meta.Sym.Arith.SemiringExpr = Lean.Grind.CommRing.Expr

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

Equations

• Lean.Meta.Sym.Arith.instInhabitedSemiring = { default := Lean.Meta.Sym.Arith.instInhabitedSemiring.default }

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

Equations

• Lean.Meta.Sym.Arith.instInhabitedRing = { default := Lean.Meta.Sym.Arith.instInhabitedRing.default }

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

Equations

• Lean.Meta.Sym.Arith.instInhabitedCommRing = { default := Lean.Meta.Sym.Arith.instInhabitedCommRing.default }

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

Equations

• Lean.Meta.Sym.Arith.instInhabitedCommSemiring = { default := Lean.Meta.Sym.Arith.instInhabitedCommSemiring.default }

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

Equations

• Lean.Meta.Sym.Arith.instInhabitedClassifyResult = { default := Lean.Meta.Sym.Arith.instInhabitedClassifyResult.default }

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

Equations

• Lean.Meta.Sym.Arith.instInhabitedState = { default := Lean.Meta.Sym.Arith.instInhabitedState.default }

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

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

Equations

• Lean.Meta.Sym.Arith.getArithState = Lean.Meta.Sym.Arith.arithExt.getState

@[inline]

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

Equations

• Lean.Meta.Sym.Arith.modifyArithState f = Lean.Meta.Sym.Arith.arithExt.modifyState f

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

Get the exponent threshold.

Equations

• Lean.Meta.Sym.Arith.getExpThreshold = do let __do_lift ← Lean.Meta.Sym.Arith.getArithState pure __do_lift.exp

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

Set the exponent threshold.

Equations

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

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

Run k with a temporary exponent threshold.

Equations

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