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