Documentation

Init.Data.PLift

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