Zulip Chat Archive

Stream: new members

Topic: rw -t : Type Error


view this post on Zulip Rene Recktenwald (May 27 2020 at 21:05):

I am doing Power World Level 5, and I solve it with

induction n with d hd,
simp,
rw pow_zero,
simp,
rw [pow_succ,add_succ,pow_succ],
rw hd,
rw mul_assoc,
refl,

Then if I change rw mul_assoc, to rw -mul_assoc, I get a type mismatch.
can somebody explain what is going on?

view this post on Zulip Johan Commelin (May 27 2020 at 21:06):

Hi Rene, you can use #backticks (that's a link) to format code.

view this post on Zulip Johan Commelin (May 27 2020 at 21:06):

Let me look up that level, while you edit your post :wink:

view this post on Zulip Kevin Buzzard (May 27 2020 at 21:06):

http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=4&level=5

view this post on Zulip Mario Carneiro (May 27 2020 at 21:06):

it's <- mul_assoc not -mul_assoc

view this post on Zulip Mario Carneiro (May 27 2020 at 21:07):

(it used to be -, so you might be looking at out of date docs)

view this post on Zulip Rene Recktenwald (May 27 2020 at 21:09):

I see, thanks


Last updated: May 14 2021 at 22:15 UTC