I am confused about what are arguments in Coq. I have read the documentation, but I have not found a formal definition of arguments thus having some confusion.
The documentation defines the syntax
intros ident+, therefore according to the definition, the argument for
intros n m can only be
n m. A Single
n is not the argument of
intros n m.
Is there anything wrong with my understanding?