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

[srghma]

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

Why useful?

Because its impossible to write function TermS.infer with Decidable

e.g.

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

wont work

The universe ladder is:

	Sort
Nonempty (Σ a, Γ ⊢ m ⇡ a)	Prop
Decidable (Nonempty ...)	Type
PDecidable (Σ a, Γ ⊢ m ⇡ a)	Type

Nonempty.elim eliminates into Prop only — it cannot reach Type. Classical.choice can, but makes everything noncomputable.