pi.nonempty

Stream: Is there code for X?

[Yaël Dillies]

Do we really not have this?

instance {α : Type*} {β : α → Type*} [Π a, nonempty (β a)] : nonempty (Π a, β a) :=
⟨λ _, classical.arbitrary _⟩

instance pi.nonempty_of_empty {α : Type*} {β : α → Type*} [is_empty α] : nonempty (Π a, β a) :=
⟨is_empty_elim⟩

[Mario Carneiro]

I thought something like that was in the classical file

[Yaël Dillies]

Ah! docs#classical.nonempty_pi

[Yaël Dillies]

Why is it not an instance? Performance reasons?

[Eric Wieser]

It's probably not there because a stronger statement is possible, docs#pi.unique_of_is_empty?

[Yaël Dillies]

Oh right. But why is the first one not an instance?

[Mario Carneiro]

it might be undesirable to use choice totally implicitly like this

[Mario Carneiro]

we don't do it for classical.prop_decidable either

[Eric Wieser]

prop_decidable would be a lot more contentious as it's not only choice but noncomputable

[Eric Wieser]

But I agree, that probably is the reason

[Mario Carneiro]

nonempty (decidable p) would be pretty similar