summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith
diff options
context:
space:
mode:
authorSon Ho2023-07-12 18:04:19 +0200
committerSon Ho2023-07-12 18:04:19 +0200
commiteb97bdb6761437e492bcf1a95b4fa43d2b69601b (patch)
tree666cf4611365dea7d9d7240870e8acbcb8dc5a4d /backends/lean/Base/Arith
parente010c10fb9a1e2d88b52a4f6b4a0865448276013 (diff)
Improve progress to use assumptions and start working on a nice syntax
Diffstat (limited to 'backends/lean/Base/Arith')
-rw-r--r--backends/lean/Base/Arith/Arith.lean42
1 files changed, 1 insertions, 41 deletions
diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean
index 20420f36..ab4fd182 100644
--- a/backends/lean/Base/Arith/Arith.lean
+++ b/backends/lean/Base/Arith/Arith.lean
@@ -11,49 +11,9 @@ import Base.Primitives
import Base.Utils
import Base.Arith.Base
-/-
-Mathlib tactics:
-- rcases: https://leanprover-community.github.io/mathlib_docs/tactics.html#rcases
-- split_ifs: https://leanprover-community.github.io/mathlib_docs/tactics.html#split_ifs
-- norm_num: https://leanprover-community.github.io/mathlib_docs/tactics.html#norm_num
-- should we use linarith or omega?
-- hint: https://leanprover-community.github.io/mathlib_docs/tactics.html#hint
-- classical: https://leanprover-community.github.io/mathlib_docs/tactics.html#classical
--/
-
-namespace List
-
- -- TODO: I could not find this function??
- @[simp] def flatten {a : Type u} : List (List a) → List a
- | [] => []
- | x :: ls => x ++ flatten ls
-
-end List
-
-namespace Lean
-
-namespace LocalContext
-
- open Lean Lean.Elab Command Term Lean.Meta
-
- -- Small utility: return the list of declarations in the context, from
- -- the last to the first.
- def getAllDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) :=
- lctx.foldrM (fun d ls => do let d ← instantiateLocalDeclMVars d; pure (d :: ls)) []
-
- -- Return the list of declarations in the context, but filter the
- -- declarations which are considered as implementation details
- def getDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) := do
- let ls ← lctx.getAllDecls
- pure (ls.filter (fun d => not d.isImplementationDetail))
-
-end LocalContext
-
-end Lean
-
namespace Arith
-open Primitives
+open Primitives Utils
-- TODO: move?
theorem ne_zero_is_lt_or_gt {x : Int} (hne : x ≠ 0) : x < 0 ∨ x > 0 := by