chore: add LinearArith/Nat/Solver.lean
This commit is contained in:
parent
043d338271
commit
137c70f055
1 changed files with 26 additions and 0 deletions
26
src/Lean/Meta/Tactic/LinearArith/Nat/Solver.lean
Normal file
26
src/Lean/Meta/Tactic/LinearArith/Nat/Solver.lean
Normal file
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue