blob: 416cd20168007b54a80d3b2e541d99dc653b74fb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
/- Arrays/slices -/
import Lean
import Lean.Meta.Tactic.Simp
import Init.Data.List.Basic
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
|
