Documentation

Lean.Meta.Tactic.LinearArith.Nat.Solver

source
structure Lean.Meta.Linear.Nat.Collect.Cnstr:
Type u_1
  • cnstr : {LinearArith : Sort u_1} → LinearArith
  • proof : Lean.Expr
source
structure Lean.Meta.Linear.Nat.Collect.State:
Type u_1
source
@[inline]
abbrev Lean.Meta.Linear.Nat.Collect.M (α : Type) :
Type
Equations