Documentation

Init.Data.PLift

source
instance instDecidableEqPLift {α✝ : Sort u_1} [DecidableEq α✝] :
DecidableEq (PLift α✝)
Equations
    source
    def instDecidableEqPLift.decEq {α✝ : Sort u_1} [DecidableEq α✝] (x✝ x✝¹ : PLift α✝) :
    Decidable (x✝ = x✝¹)
    Equations
      Instances For
        source
        instance instSubsingletonPLift {α : Sort u_1} [Subsingleton α] :
        Subsingleton (PLift α)