Documentation
Init
.
Data
.
Array
.
DecidableEq
Search
Google site search
return to top
source
Imports
Init.ByCases
Init.Data.Array.Basic
Imported by
Array
.
eq_of_isEqvAux
Array
.
eq_of_isEqv
Array
.
isEqvAux_self
Array
.
isEqv_self
Array
.
instDecidableEq
source
@[irreducible]
theorem
Array
.
eq_of_isEqvAux
{α :
Type
u_1}
[
DecidableEq
α
]
(a :
Array
α
)
(b :
Array
α
)
(hsz :
a
.size
=
b
.size
)
(i :
Nat
)
(hi :
i
≤
a
.size
)
(heqv :
a
.isEqvAux
b
hsz
(
fun (
x
y
:
α
) =>
decide
(
x
=
y
)
)
i
=
true
)
(j :
Nat
)
(low :
i
≤
j
)
(high :
j
<
a
.size
)
:
a
[
j
]
=
b
[
j
]
source
theorem
Array
.
eq_of_isEqv
{α :
Type
u_1}
[
DecidableEq
α
]
(a :
Array
α
)
(b :
Array
α
)
:
(
a
.isEqv
b
fun (
x
y
:
α
) =>
decide
(
x
=
y
)
)
=
true
→
a
=
b
source
@[irreducible]
theorem
Array
.
isEqvAux_self
{α :
Type
u_1}
[
DecidableEq
α
]
(a :
Array
α
)
(i :
Nat
)
:
a
.isEqvAux
a
⋯
(
fun (
x
y
:
α
) =>
decide
(
x
=
y
)
)
i
=
true
source
theorem
Array
.
isEqv_self
{α :
Type
u_1}
[
DecidableEq
α
]
(a :
Array
α
)
:
(
a
.isEqv
a
fun (
x
y
:
α
) =>
decide
(
x
=
y
)
)
=
true
source
instance
Array
.
instDecidableEq
{α :
Type
u_1}
[
DecidableEq
α
]
:
DecidableEq
(
Array
α
)
Equations
a
.instDecidableEq
b
=
match h :
a
.isEqv
b
fun (
a
b
:
α
) =>
decide
(
a
=
b
)
with |
true
=>
isTrue
⋯
|
false
=>
isFalse
⋯