horrible typo in current web version

[kbuzzard]

Right now live on the website we have

This is a horrible typo in the docs (succ a -> succ b) because it's confusing. It was fixed on main in this commit. Can this be deployed? And is there a clever way of stopping this happening in future?

[abentkamp]

I've deployed it. (hopefully without breaking anything else?)

I don't think such typos can be avoided. What do you have in mind?

[kbuzzard]

I was wondering whether we could get Lean to write the text statement from the Lean statement. But having now written a bunch of levels I see that this is unfeasible, I agree that we need the flexibility to make typos.