Documentation
Mathlib
.
Init
.
Data
.
List
.
Instances
Search
Google site search
Mathlib
.
Init
.
Data
.
List
.
Instances
source
Imports
Init
Mathlib.Init.Data.List.Lemmas
Imported by
List
.
decidableBex
List
.
decidableBall
Decidable Instances for
List
not (yet) in
Std
source
ink
instance
List
.
decidableBex
{α :
Type
u_1}
{p :
α
→
Prop
}
[inst :
DecidablePred
p
]
(l :
List
α
)
:
Decidable
(
∃
x
,
x
∈
l
∧
p
x
)
Equations
One or more equations did not get rendered due to their size.
List.decidableBex
[]
=
isFalse
(_ :
¬
∃
x
,
x
∈
[]
∧
p
x
)
source
ink
instance
List
.
decidableBall
{α :
Type
u_1}
{p :
α
→
Prop
}
[inst :
DecidablePred
p
]
(l :
List
α
)
:
Decidable
(
(
x
:
α
) →
x
∈
l
→
p
x
)
Equations
List.decidableBall
l
=
if h :
∃
x
,
x
∈
l
∧
¬
p
x
then
isFalse
(_ :
¬
(
(
x
:
α
) →
x
∈
l
→
p
x
)
)
else
isTrue
(
List.decidableBall.proof_2
l
h
)