structure Lean.Meta.Grind.Arith.Linear.OfNatModuleM.Context : Type

• natStructId : Nat

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Linear.OfNatModuleM (α : Type) : Type

Equations

• Lean.Meta.Grind.Arith.Linear.OfNatModuleM = ReaderT Lean.Meta.Grind.Arith.Linear.OfNatModuleM.Context Lean.Meta.Grind.GoalM

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Linear.OfNatModuleM.run {α : Type} (natStructId : Nat) (x : OfNatModuleM α) : GoalM α

Equations

• Lean.Meta.Grind.Arith.Linear.OfNatModuleM.run natStructId x = x { natStructId := natStructId }

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Linear.getNatStructId : OfNatModuleM Nat

Equations

• Lean.Meta.Grind.Arith.Linear.getNatStructId = do let __do_lift ← read pure __do_lift.natStructId

def Lean.Meta.Grind.Arith.Linear.getNatStruct : OfNatModuleM NatStruct

Equations

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

def Lean.Meta.Grind.Arith.Linear.OfNatModuleM.getStruct : OfNatModuleM Struct

Equations

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

instance Lean.Meta.Grind.Arith.Linear.instMonadGetStructOfNatModuleM : MonadGetStruct OfNatModuleM

Equations

• Lean.Meta.Grind.Arith.Linear.instMonadGetStructOfNatModuleM = { getStruct := Lean.Meta.Grind.Arith.Linear.OfNatModuleM.getStruct }

@[inline]

def Lean.Meta.Grind.Arith.Linear.modifyNatStruct (f : NatStruct → NatStruct) : OfNatModuleM Unit

Equations

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

def Lean.Meta.Grind.Arith.Linear.getTermNatStructId? (e : Expr) : GoalM (Option Nat)

Equations

• Lean.Meta.Grind.Arith.Linear.getTermNatStructId? e = do let __do_lift ← Lean.Meta.Grind.Arith.Linear.get' pure (Lean.PersistentHashMap.find? __do_lift.exprToNatStructId { expr := e })

def Lean.Meta.Grind.Arith.Linear.inSameNatStruct? (a b : Expr) : GoalM (Option Nat)

Returns some natStructId if a and b are elements of the same NatModule structure.

Equations

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

def Lean.Meta.Grind.Arith.Linear.setTermNatStructId (e : Expr) : OfNatModuleM Unit

Equations

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

def Lean.Meta.Grind.Arith.Linear.ofNatModule (e : Expr) : OfNatModuleM (Expr × Expr)

Equations

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

def Lean.Meta.Grind.Arith.Linear.normNatModuleDiseq (a b : Expr) : OfNatModuleM Unit

Equations

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