How can we have a 2-element tuple with both elements bound to a different name when making a function accepting this tuple as argument?

Something like:

```
Definition foo ((a,b) : (nat * nat)): nat := a.
(* doesn't work
Syntax error: [Prim.name] expected after '(' (in [constr:closed_binder]).
*)
```

Following works though.

```
Check (3,2): (nat*nat). (* works *)
```

```
Definition foo '((a,b) : (nat * nat)): nat := a.
```

Thanks. What does the `'`

do? Is there a place where I can read more about it?

It allows binders to be patterns, here's the refman entry (though it's very terse on the topic): https://coq.inria.fr/distrib/current/refman/language/core/assumptions.html

Thanks again.

Ju-sh has marked this topic as resolved.

Last updated: Oct 04 2023 at 20:01 UTC