blob: a268bcbabcc898c515a5eade07367d4cce0a9e3d (
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 core.ops.range.Range (α : Type u) where
mk ::
start: α
end_: α
end Primitives
|
