[ doc ] Update documentation for with

[dunhamsteve]

Description

The documentation in :doc with mentions that with rewrites the target type. This doesn't seem to be mentioned in the html documentation, so I'm copying it here. This came up in the discussion in #3271.

I've also added documentation for multi-with and removed the warning about the documentation not being updated for Idris 2. The documentation appears to be accurate and all of the code snippets run in Idris 2.

#3271 also asks when to use with vs case. I'm not sure what to say or where to say it, so I haven't addressed that.

[buzden]

#3271 also asks when to use with vs case. I'm not sure what to say or where to say it, so I haven't addressed that.

The great difference is that with rewrites types of all arguments according to the information given by dependent pattern matching. Say, you have xs : Vect n a and ys : Vect m a. Say, you pattern match on a value Dec (n = m) in your with. This means that in the clause Yes Refl you will get both xs and ys to be of type Vect m a. And wherever n appeared in the types of arguments, it will be replaced by m in this clause.