From f7c09787c4a7457568d3d79d38b45caac4af8772 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 4 Aug 2023 18:19:37 +0200
Subject: Start adding support for Arrays/Slices in the Lean library

---
 backends/lean/Base/Primitives/Range.lean | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 backends/lean/Base/Primitives/Range.lean

(limited to 'backends/lean/Base/Primitives/Range.lean')

diff --git a/backends/lean/Base/Primitives/Range.lean b/backends/lean/Base/Primitives/Range.lean
new file mode 100644
index 00000000..26cbee42
--- /dev/null
+++ b/backends/lean/Base/Primitives/Range.lean
@@ -0,0 +1,19 @@
+/- Arrays/slices -/
+import Lean
+import Lean.Meta.Tactic.Simp
+import Init.Data.List.Basic
+import Mathlib.Tactic.RunCmd
+import Mathlib.Tactic.Linarith
+import Base.IList
+import Base.Primitives.Scalar
+import Base.Arith
+import Base.Progress.Base
+
+namespace Primitives
+
+structure Range (α : Type u) where
+  mk ::
+  start: α
+  end_: α
+
+end Primitives
-- 
cgit v1.2.3