@[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
• natSMulFn? : Option Expr

@[instance_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
• natSMulFn? : Option Expr
• intSMulFn? : Option Expr
• one? : Option Expr

@[instance_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.CommRing extends 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
• natSMulFn? : Option Expr
• intSMulFn? : Option Expr
• one? : Option Expr
• invFn? : Option Expr

  Inverse function if fieldInst? is some inst

• divFn? : Option Expr

  Division 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.

• powIdentityInst? : Option (Expr × Expr × Nat)

  PowIdentity instance, the synthesized CommSemiring instance, and exponent p if available.

@[instance_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.CommSemiring extends 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
• natSMulFn? : 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

@[instance_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.

@[instance_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.Order : Type

Classification state for a type with an IsPreorder instance: the order instances, the canonical ≤/< functions, and the link to the ring classification when the type is also an ordered ring.

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

  Cached getDecLevel type

• isPreorderInst : Expr
• leInst : Expr

  LE instance

• ltInst? : Option Expr

  LT instance if available

• isPartialInst? : Option Expr

  IsPartialOrder instance if available

• isLinearPreInst? : Option Expr

  IsLinearPreorder instance if available

• lawfulOrderLTInst? : Option Expr

  LawfulOrderLT instance if available

• ringId? : Option Nat

  Id of the CommRing (rings) or non-commutative Ring (ncRings) classification, if available.

• isCommRing : Bool

  true if ringId? indexes rings, false if it indexes ncRings

• semiringId? : Option Nat

  Id of the semiring classification (semirings or ncSemirings) when the type is an ordered semiring that is not a ring.

• isCommSemiring : Bool

  true if semiringId? indexes semirings, false if it indexes ncSemirings

• ringInst? : Option Expr

  Ring instance if available

• orderedRingInst? : Option Expr

  OrderedRing instance if available (with the semiring instance of ringId?, or of semiringId?)

• leFn : Expr

  Canonical LE.le type leInst

• ltFn? : Option Expr

  Canonical LT.lt type ltInst, present iff lawfulOrderLTInst? is

@[instance_reducible]

instance Lean.Meta.Sym.Arith.instInhabitedOrder : Inhabited Order

Equations

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

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

Arith type classification state, stored as a SymExtension.

• exp : Nat

  Maximum exponent eagerly evaluated while computing bounds for ToInt and the characteristic of a ring. Same meaning as Grind.Config.exp.

• 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.

• orders : Array Order

  Order structures.

• typeOrderClassify : PHashMap ExprPtr (Option Nat)

  Mapping from types to their order id. Caches failures as none.

@[instance_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.