Zulip Chat Archive

Stream: general

Topic: Friday afternoon fun: guess the goals


view this post on Zulip Kevin Buzzard (Nov 27 2020 at 18:36):

import tactic

example (a b : ) : false :=
begin
  have hab : {a}  {b} = {a, b},
  { library_search },
  all_goals {sorry}
end

Compiles fine. As Mario once said -- be the elaborator. What do you the the goals closed by sorry are? Again this was something that came up at Xena last night (whilst trying to do an integral!)

view this post on Zulip Johan Commelin (Nov 27 2020 at 18:46):

false and decidable_eq nat?

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 18:48):

You forgot has_singleton ℕ unit (and several others)

view this post on Zulip Floris van Doorn (Nov 27 2020 at 18:49):

I'm not even sure if Lean can figure out the have is talking about set nat. So I'm guessing something like ?m and has_singleton nat ?m

view this post on Zulip Floris van Doorn (Nov 27 2020 at 18:49):

or maybe has_singleton nat (set ?m)

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 18:50):

Here I'll give you an easier one:

import tactic
import data.complex.basic

example (a b : ) : false :=
begin
  have hab : {a}  {b} = {a, b},
    apply complex.ext,
  all_goals {sorry}
end

Last updated: May 09 2021 at 19:11 UTC