Documentation

Init.Data.ULift

source
instance instDecidableEqULift {α✝ : Type u_1} [DecidableEq α✝] :
DecidableEq (ULift α✝)
Equations
    source
    def instDecidableEqULift.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : ULift α✝) :
    Decidable (x✝ = x✝¹)
    Equations
      Instances For
        source
        instance instSubsingletonULift {α : Type u_1} [Subsingleton α] :
        Subsingleton (ULift α)