# Arguments in tactics

**URL:** <https://discourse.rocq-prover.org/t/arguments-in-tactics/922>\
**Category:** Using Rocq\
**Created:** [July 5, 2020, 10:08am UTC](https://discourse.rocq-prover.org/t/arguments-in-tactics/922 "2020-07-05T10:08:27Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![ZWY](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zwy/32/335_2.png) [@ZWY](https://discourse.rocq-prover.org/u/ZWY)\
**Post date:** [July 5, 2020, 10:08am UTC](https://discourse.rocq-prover.org/t/arguments-in-tactics/922/1 "2020-07-05T10:08:28Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![nojb](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/nojb/32/256_2.png) [@nojb](https://discourse.rocq-prover.org/u/nojb)\
**Post date:** [July 5, 2020, 10:20am UTC](https://discourse.rocq-prover.org/t/arguments-in-tactics/922/2 "2020-07-05T10:20:54Z")

</div>

`ident+` refers to a sequence of one or more `ident`s, so indeed a single `n` is a valid argument to `intros`.

Cheers,  
Nicolás