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

Equations

• Lean.Meta.Grind.Arith.Linear.get' = Lean.Meta.Grind.Arith.Linear.linearExt.getState

@[inline]

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

Equations

• Lean.Meta.Grind.Arith.Linear.modify' f = Lean.Meta.Grind.Arith.Linear.linearExt.modifyState f

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

@[always_inline]

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

Equations

• Lean.Meta.Grind.Arith.Linear.instMonadGetStructOfMonadLift m n = { getStruct := liftM Lean.Meta.Grind.Arith.Linear.getStruct }

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.Arith.Linear.LinearM.run structId x = x { structId := structId }

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.Arith.Linear.getStructId = do let __do_lift ← read pure __do_lift.structId

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

Equations

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

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

Equations

• Lean.Meta.Grind.Arith.Linear.instMonadGetStructLinearM = { getStruct := Lean.Meta.Grind.Arith.Linear.LinearM.getStruct }

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

Equations

• Lean.Meta.Grind.Arith.Linear.getRingCore? (some ringId) = Lean.Meta.Grind.Arith.CommRing.RingM.run ringId do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getRing pure (some __do_lift)
• Lean.Meta.Grind.Arith.Linear.getRingCore? ringId? = pure none

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

Equations

• Lean.Meta.Grind.Arith.Linear.throwNotRing = Lean.throwError (Lean.toMessageData "`grind linarith` internal error, structure is not a ring")

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

Equations

• Lean.Meta.Grind.Arith.Linear.throwNotCommRing = Lean.throwError (Lean.toMessageData "`grind linarith` internal error, structure is not a commutative ring")

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

Equations

• Lean.Meta.Grind.Arith.Linear.getRing? = do let __do_lift ← Lean.Meta.Grind.Arith.Linear.getStruct liftM (Lean.Meta.Grind.Arith.Linear.getRingCore? __do_lift.ringId?)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[inline]

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

Equations

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