Zulip Chat Archive

Stream: general

Topic: What happened next?

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

Kevin Buzzard (Apr 04 2018 at 19:51):

Took me slightly by surprise at the time.

Mario Carneiro (Apr 04 2018 at 20:07):

heh, I assume 2 got rewritten?

Kevin Buzzard (Apr 04 2018 at 20:27):

That was part of it.

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

Kevin Buzzard (Apr 04 2018 at 20:30):

Oh I have just realised what is going on.

Kevin Buzzard (Apr 04 2018 at 20:30):

So the goal becomes

Kevin Buzzard (Apr 04 2018 at 20:30):

bit0 x = y

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: Dec 20 2023 at 11:08 UTC