rw -t : Type Error

Stream: new members

[Rene Recktenwald]

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?

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Mario Carneiro]

it's <- mul_assoc not -mul_assoc

[Mario Carneiro]

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

[Rene Recktenwald]

I see, thanks