mapply

Stream: mathlib4

[Moritz Doll]

Hi,
I have some questions regarding my assignment.
1) Am I correct in assuming the difference between the Lean3 version and the Lean4 version will be that the Lean4 version of mapply uses apply with a higher MetavarContext depth instead of the flag?
2) I am not fully understanding what is meant in the Lean3 documentation by "matching" instead of "unification". My working knowledge is that apply (or refine) create new meta-variables and then put a partial proof-term into the goal meta-variable (please correct me if I am using the wrong words or I am misunderstanding something) and I guess is referred to as unification. What is matching?
3) mapply seems to have no tests and is not used anywhere in mathlib, are there any examples on what mapply succeeds on which apply cannot do. There might be the related question whether mapply is useful to have in the first place, but for the sake of tactics porting this is of course not relevant.

[Mario Carneiro]

If mapply isn't used in mathlib, we can probably skip it