Documentation
Init
.
Data
.
PLift
Search
return to top
source
Imports
Init.Core
Imported by
instDecidableEqPLift
instDecidableEqPLift
.
decEq
instSubsingletonPLift
source
instance
instDecidableEqPLift
{
α✝
:
Sort
u_1}
[
DecidableEq
α✝
]
:
DecidableEq
(
PLift
α✝
)
Equations
instDecidableEqPLift
=
instDecidableEqPLift.decEq
source
def
instDecidableEqPLift
.
decEq
{
α✝
:
Sort
u_1}
[
DecidableEq
α✝
]
(
x✝
x✝¹
:
PLift
α✝
)
:
Decidable
(
x✝
=
x✝¹
)
Equations
instDecidableEqPLift.decEq
{
down
:=
a
}
{
down
:=
b
}
=
if h :
a
=
b
then
h
▸
isTrue
⋯
else
isFalse
⋯
Instances For
source
instance
instSubsingletonPLift
{
α
:
Sort
u_1}
[
Subsingleton
α
]
:
Subsingleton
(
PLift
α
)