HepLean Documentation
Init
.
Data
.
List
.
Nat
.
BEq
Search
Google site search
return to top
source
Imports
Init.Data.List.Basic
Init.Data.Nat.Lemmas
Imported by
List
.
isEqv_eq_decide
List
.
beq_eq_isEqv
List
.
beq_eq_decide
isEqv
#
source
theorem
List
.
isEqv_eq_decide
{α :
Type
u_1}
(a b :
List
α
)
(r :
α
→
α
→
Bool
)
:
a
.isEqv
b
r
=
if h :
a
.length
=
b
.length
then
decide
(∀ (
i
:
Nat
) (
h'
:
i
<
a
.length
),
r
a
[
i
]
b
[
i
]
=
true
)
else
false
beq
#
source
theorem
List
.
beq_eq_isEqv
{α :
Type
u_1}
[
BEq
α
]
(a b :
List
α
)
:
a
.beq
b
=
a
.isEqv
b
fun (
x1
x2
:
α
) =>
x1
==
x2
source
theorem
List
.
beq_eq_decide
{α :
Type
u_1}
[
BEq
α
]
(a b :
List
α
)
:
(
a
==
b
)
=
if h :
a
.length
=
b
.length
then
decide
(∀ (
i
:
Nat
) (
h'
:
i
<
a
.length
),
(
a
[
i
]
==
b
[
i
]
)
=
true
)
else
false