@[instance_reducible]

instance instDecidableEqULift {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (ULift α✝)

Equations

• instDecidableEqULift = instDecidableEqULift.decEq

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 ⋯

instance instSubsingletonULift {α : Type u_1} [Subsingleton α] : Subsingleton (ULift α)