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

• cnstr : {LinearArith : Sort u_1} → LinearArith
• proof : Lean.Expr

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

• 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