Zulip Chat Archive

Stream: new members

Topic: inhabited should be nonempty

Joachim Breitner (Mar 26 2022 at 15:28):

I am getting

free_group.injective_lift_of_ping_pong - The following `inhabited` instances should be `nonempty`. argument 2: [_inst_3 : inhabited ι]

from the linter. I can change that parameter, but what do I use instead of default ι in my proofs now?

Yaël Dillies (Mar 26 2022 at 15:32):


Joachim Breitner (Mar 26 2022 at 15:35):

Ah, thanks. I was already doing things like

    exact nonempty.elim (by apply_instance) (λ (i : ι),
      begin  end)


Joachim Breitner (Mar 26 2022 at 15:36):

Maybe I’ll add a pointer to classical.arbitrary from https://leanprover-community.github.io/mathlib_docs/init/logic.html#nonempty? Ah, but that doesn’t work because it’d point form core into mathlib. I’ll maybe improve the linter message then.

Hmm, but that would lose some conciseness there. I’ll leave it and let others learn via Zulip as well :-)

Joachim Breitner (Mar 26 2022 at 15:41):

I’ll leave a question on the SE site, for future users googling for this.
@Yaël Dillies , do you want to answer https://proofassistants.stackexchange.com/questions/1168/like-arbitrary-but-for-nonempty-instead-of-inhabited for SE reputation points, or should I just do it?

Yaël Dillies (Mar 26 2022 at 15:41):

Oh I guess I should because I still haven't been active at all here.

Joachim Breitner (Mar 26 2022 at 15:42):

I wonder if there is a black market for SE rep points already, where people pay with lines of lean proof scripts…

Eric Rodriguez (Mar 26 2022 at 16:32):

there's also the inhabit tactic if you want to keep using default

Eric Wieser (Mar 26 2022 at 17:02):


Last updated: Dec 20 2023 at 11:08 UTC