Documentation

Lean.Meta.Tactic.LinearArith.Nat.Solver

source
inductive Lean.Meta.Linear.Nat.Collect.LinearArith :
Type
    Instances For
      source
      structure Lean.Meta.Linear.Nat.Collect.Cnstr :
      Type
      Instances For
        source
        structure Lean.Meta.Linear.Nat.Collect.State :
        Type
        Instances For
          source
          @[inline, reducible]
          abbrev Lean.Meta.Linear.Nat.Collect.M (α : Type) :
          Type
          Equations
          Instances For