Add `PDecidable` (like `Decidable`, but allows arbitrary sorts so it can hold data)

module

public import Mathlib.Logic.IsEmpty.Defs

/--
`PDecidable` is like `Decidable`, but allows arbitrary sorts so it can hold data.
-/
class inductive PDecidable (α : Sort _) where
  /-- Proves that `α` is empty by supplying a proof of `IsEmpty α` -/
  | isFalse (h : IsEmpty α) : PDecidable α
  /-- Proves that `α` is inhabited by supplying a datum of `α` -/
  | isTrue (h : α) : PDecidable α

namespace PDecidable
  def toDecidable : PDecidable α → Decidable (Nonempty α)
  | .isTrue a => .isTrue ⟨a⟩
  | .isFalse na => .isFalse (fun ⟨a⟩ => na.false a)

  /-- Safely extracts the data, but forces you to prove it isn't `isFalse` first. -/
  def get (d : PDecidable α) (h : Nonempty α) : α :=
    match d with
    | .isTrue a => a
    | .isFalse na => False.elim (h.elim na.false)
end PDecidable

instance [Repr α] : Repr (PDecidable α) where
  reprPrec da n := match da with
  | .isTrue a => ".isTrue " ++ reprPrec a n
  | .isFalse _ => ".isFalse _"

very useful class, used in PLFaLean

mutual
  def TermS.infer' (m : TermS) (Γ : Context) : Decidable (Nonempty (Σ a, Γ ⊢ m ⇡ a)) :=
  def TermI.infer' (m : TermI) (Γ : Context) (a : Ty) : Decidable (Nonempty (Γ ⊢ m ⇣ a)) :=
end

Start by reading Mathlib.Logic.IsEmpty.Defs and the proposed PDecidable declaration, then compare its intended use with TermS.infer' and TermI.infer' in the linked PLFaLean files. Done means the class and its shown helpers support arbitrary sorts while preserving the intended computational use, with behavior checked against the motivating inference scenario.