@[implicit_reducible]

instance instDecidableEqPLift {α✝ : Sort u_1} [DecidableEq α✝] : DecidableEq (PLift α✝)

Equations

• instDecidableEqPLift = instDecidableEqPLift.decEq

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 ⋯

instance instSubsingletonPLift {α : Sort u_1} [Subsingleton α] : Subsingleton (PLift α)