HepLean Documentation

Lean.Meta.Tactic.LinearArith.Nat.Solver

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

Instances For

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

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

Instances For

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

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

Instances For

@[reducible, inline]

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

Equations

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

Instances For