Element of type or proof that it is empty?

Stream: Is there code for X?

[E M]

What is the idiomatic way of representing a function that either returns an element of a type, or a proof that there is no such element?

In other words, is there a Decidable equivalent in Type instead of Prop in std/mathlib?

Should one just return an Option and provide a proof that if it is none, then the type is uninhabited?

[Yaël Dillies]

That is one option, indeed. If you want something that exactly does "either returns an element of a type, or a proof that there is no such element", it would be α ⊕' IsEmpty α

[Eric Wieser]

This has been discussed enough that perhaps Mathlib should provide such a thing

[Eric Wieser]

See for instance https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/if-in-Type/near/241090877