blob: 26cbee42d65027d2a51796ccb9c5f933268e3273 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
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
|
