inductive Lean.Meta.Linear.Nat.Collect.LinearArith : Type

structure Lean.Meta.Linear.Nat.Collect.Cnstr : Type

• cnstr : Lean.Meta.Linear.Nat.Collect.LinearArith
• proof : Lean.Expr

structure Lean.Meta.Linear.Nat.Collect.State : Type

• cnstrs : Array Lean.Meta.Linear.Nat.Collect.Cnstr

@[inline]

abbrev Lean.Meta.Linear.Nat.Collect.M (α : Type) : Type

Equations

• Lean.Meta.Linear.Nat.Collect.M = StateRefT' IO.RealWorld Lean.Meta.Linear.Nat.Collect.State Lean.Meta.Linear.Nat.ToLinear.M