empty types

Stream: general

[Johan Commelin]

We have empty, pempty, and fin 0. Possibly more. Should there be a typeclass that abstracts over empty types? How do we make it play nicely with [nonempty X]?

Question is inspired by https://github.com/leanprover-community/mathlib/pull/5520/files#diff-713f1ae1a0f3e41d74048db22cbe6705516ab077f6e352f19b46d29a230b9a2cR150

[Kevin Buzzard]

I think we have finite and infinite?

[Yury G. Kudryashov]

We can have

class is_empty (α : Sort*) : Prop := (to_False : α → False)

lemma is_empty_or_nonempty (α : Sort*) : is_empty α ∨ nonempty α := sorry

Then tactic#inhabit can try cases is_empty_or_nonempty α, { resetI, simp } like tactic#nontriviality

[Reid Barton]

False? have you been playing with Lean 4?

[Yury G. Kudryashov]

No, I guess this is from Python.