i'm just playing around with lean lol

Stream: new members

[Huỳnh Trần Khanh]

What does classical.choice x._proof_1 1 = classical.choice x._proof_1 2 mean?

noncomputable def x : ℕ → string := classical.choice nonempty_of_inhabited

lemma this_should_be_unprovable_right : x 1 = x 2 := begin
  rw x,
end

[Huỳnh Trần Khanh]

like the _proof_1 thing looks really strange to me

[Kyle Miller]

If you do

#print x
#print x._proof_1

you can see

noncomputable def x : ℕ → string :=
classical.choice x._proof_1

and

theorem x._proof_1 : nonempty (ℕ → string) :=
nonempty_of_inhabited

Lean tends to generate many underscore functions when it creates definitions (especially for pattern matching). I'm not sure why it split off this nonempty instance like this.

[Mario Carneiro]

And indeed, that theorem is unprovable. What you have done is choose a "random" function ℕ → string using choice, and for such a function we know nothing about its values besides the type, so x 1 : string may or may not be equal to x 2 : string