def Lean.Meta.Grind.Arith.Linear.get' : GoalM State

@[inline]

def Lean.Meta.Grind.Arith.Linear.modify' (f : State → State) : GoalM Unit

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

• structId : Nat

class Lean.Meta.Grind.Arith.Linear.MonadGetStruct (m : Type → Type) : Type

• getStruct : m Struct

@[implicit_reducible, always_inline]

instance Lean.Meta.Grind.Arith.Linear.instMonadGetStructOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadGetStruct m] : MonadGetStruct n

@[reducible, inline]

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

We don't want to keep carrying the StructId around.

@[reducible, inline]

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

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Linear.getStructId : LinearM Nat

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

@[implicit_reducible]

instance Lean.Meta.Grind.Arith.Linear.instMonadGetStructLinearM : MonadGetStruct LinearM

def Lean.Meta.Grind.Arith.Linear.getRingCore? (ringId? : Option Nat) : GoalM (Option CommRing.Ring)

def Lean.Meta.Grind.Arith.Linear.throwNotRing {α : Type} : LinearM α

def Lean.Meta.Grind.Arith.Linear.throwNotCommRing {α : Type} : LinearM α

def Lean.Meta.Grind.Arith.Linear.getRing? : LinearM (Option CommRing.Ring)

@[implicit_reducible]

instance Lean.Meta.Grind.Arith.Linear.instMonadCanonLinearM : CommRing.MonadCanon LinearM

def Lean.Meta.Grind.Arith.Linear.LinearM.getRing : LinearM CommRing.Ring

@[implicit_reducible]

instance Lean.Meta.Grind.Arith.Linear.instMonadRingLinearM : CommRing.MonadRing LinearM

def Lean.Meta.Grind.Arith.Linear.withRingM {α : Type} (x : CommRing.RingM α) : LinearM α

@[inline]

def Lean.Meta.Grind.Arith.Linear.modifyStruct (f : Struct → Struct) : LinearM Unit