Zulip Chat Archive

Stream: general

Topic: What happened next?


view this post on Zulip Kevin Buzzard (Apr 04 2018 at 19:50):

example (d : ℕ) (H : 1  =  2  * nat.succ d) : 1  =  2  * d +  2  :=
begin
rw H,
-- goal now?
admit,
end

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 19:51):

Took me slightly by surprise at the time.

view this post on Zulip Mario Carneiro (Apr 04 2018 at 20:07):

heh, I assume 2 got rewritten?

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 20:27):

That was part of it.

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 20:29):

The other phenomenon shows itself here:

example (x y : ) (H : 1 = x) : 2 = y :=
begin
rw H,
-- goal now?
admit,
end

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 20:30):

Oh I have just realised what is going on.

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 20:30):

So the goal becomes

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 20:30):

bit0 x = y

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 20:31):

but that's because 2 isn't defined to be succ 1 here, it's defined to be bit0 1


Last updated: May 16 2021 at 22:14 UTC