No introduction of "backwards rewrite"

[Madjosz]

Implication world, Level 4
After executing the rw [four_eq_succ_three] at h the next step in the guide writes

Now rewrite succ_eq_add_one backwards at h to get the right hand side.

but nowhere before it is explained that backwards is done by ←. I assume it was removed with #8. One can only see this by pressing "Show more help!" (which spoiles the whole solution) or reading the documentation of rw. While the latter is of course a crucial ability for using programming languages I would prefer to be taught this explicitly.

[joneugster]

Thanks for reporting, modified the hint message.

[joneugster]

@kbuzzard or would you want to add a dedicated level to teach rw [← my_theorem] somewhere?

[kbuzzard]

Teaching it explicitly is a great idea! I'll add a level to tutorial world.

[Madjosz]

Fixed with d80a520