Documentation
Batteries
.
Data
.
Range
.
Lemmas
Search
Google site search
return to top
source
Imports
Init
Batteries.Tactic.SeqFocus
Batteries.Data.List.Lemmas
Batteries.Data.List.Init.Attach
Imported by
Std
.
Range
.
numElems
Std
.
Range
.
numElems_stop_le_start
Std
.
Range
.
numElems_step_1
Std
.
Range
.
mem_range'_elems
Std
.
Range
.
forIn'_eq_forIn_range'
Std
.
Range
.
forIn_eq_forIn_range'
source
def
Std
.
Range
.
numElems
(r :
Std.Range
)
:
Nat
The number of elements contained in a
Std.Range
.
Equations
r
.numElems
=
if
r
.step
=
0
then
if
r
.stop
≤
r
.start
then
0
else
r
.stop
else
(
r
.stop
-
r
.start
+
r
.step
-
1
)
/
r
.step
Instances For
source
theorem
Std
.
Range
.
numElems_stop_le_start
(r :
Std.Range
)
:
r
.stop
≤
r
.start
→
r
.numElems
=
0
source
theorem
Std
.
Range
.
numElems_step_1
(start :
Nat
)
(stop :
Nat
)
:
{
start
:=
start
,
stop
:=
stop
,
step
:=
1
}
.numElems
=
stop
-
start
source
theorem
Std
.
Range
.
mem_range'_elems
{x :
Nat
}
(r :
Std.Range
)
(h :
x
∈
List.range'
r
.start
r
.numElems
r
.step
)
:
x
∈
r
source
theorem
Std
.
Range
.
forIn'_eq_forIn_range'
{m :
Type
u_1 →
Type
u_2
}
{β :
Type
u_1}
[
Monad
m
]
(r :
Std.Range
)
(init :
β
)
(f :
(
a
:
Nat
) →
a
∈
r
→
β
→
m
(
ForInStep
β
)
)
:
forIn'
r
init
f
=
forIn
(
List.pmap
Subtype.mk
(
List.range'
r
.start
r
.numElems
r
.step
)
⋯
)
init
fun (
x
:
{
x
:
Nat
//
x
∈
r
}
) =>
match (motive :=
{
x
:
Nat
//
x
∈
r
}
→
β
→
m
(
ForInStep
β
)
)
x
with |
⟨
a
,
h
⟩
=>
f
a
h
source
theorem
Std
.
Range
.
forIn_eq_forIn_range'
{m :
Type
u_1 →
Type
u_2
}
{β :
Type
u_1}
[
Monad
m
]
(r :
Std.Range
)
(init :
β
)
(f :
Nat
→
β
→
m
(
ForInStep
β
)
)
:
forIn
r
init
f
=
forIn
(
List.range'
r
.start
r
.numElems
r
.step
)
init
f