buzden
commented
1 month ago 3271 also asks when to use
withvscase. 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.
Description
The documentation in
:doc withmentions thatwithrewrites 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-
withand 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
withvscase. I'm not sure what to say or where to say it, so I haven't addressed that.