Finset.Nonempty

Stream: mathlib4

[María Inés de Frutos Fernández]

The following #mwe results in the error type expected, got (hs : s.Nonempty). Any suggestions? Thanks!

import Mathlib.Data.Fintype.Basic

-- type expected, got (hs : s.Nonempty)
example {ι : Type*} {s : Finset ι} (hs : s.Nonempty): true := by
  have h : ∃ (x : s) (hs' : (hs → true)), true := sorry
  sorry

[Ruben Van de Velde]

What do you think (hs → true) means there?

[María Inés de Frutos Fernández]

"If the finset s is nonempty, then true".

[Yaël Dillies]

That would be s.Nonempty → True

[María Inés de Frutos Fernández]

Oh, sorry, I now see what I caused my confusion (this mwe was coming from a ported file; I was mixing up univ_nonempty and univ.Nonempty). Thanks.