From 137c70f055e6d73f2a074b28faab7373a6fa4710 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 3 Mar 2022 11:13:40 -0800 Subject: [PATCH] chore: add `LinearArith/Nat/Solver.lean` --- .../Meta/Tactic/LinearArith/Nat/Solver.lean | 26 +++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 src/Lean/Meta/Tactic/LinearArith/Nat/Solver.lean diff --git a/src/Lean/Meta/Tactic/LinearArith/Nat/Solver.lean b/src/Lean/Meta/Tactic/LinearArith/Nat/Solver.lean new file mode 100644 index 0000000000..8fe6126788 --- /dev/null +++ b/src/Lean/Meta/Tactic/LinearArith/Nat/Solver.lean @@ -0,0 +1,26 @@ +/- +Copyright (c) 2022 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +import Lean.Meta.Tactic.LinearArith.Solver +import Lean.Meta.Tactic.LinearArith.Nat.Basic + +namespace Lean.Meta.Linear.Nat + +namespace Collect + +structure Cnstr where + cnstr : LinearArith + proof : Expr + +structure State where + cnstrs : Array Cnstr + +abbrev M := StateRefT State ToLinear.M + +-- TODO + +end Collect + +end Lean.Meta.Linear.Nat