Stream: Coq users

Topic: ✔ 'Decomposed' tuple as function argument


view this post on Zulip Julin S (Dec 21 2021 at 15:53):

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 *)

view this post on Zulip Li-yao (Dec 21 2021 at 15:56):

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

view this post on Zulip Julin S (Dec 21 2021 at 16:02):

Thanks. What does the ' do? Is there a place where I can read more about it?

view this post on Zulip Li-yao (Dec 21 2021 at 16:07):

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

view this post on Zulip Julin S (Dec 21 2021 at 16:08):

Thanks again.

view this post on Zulip Notification Bot (Dec 21 2021 at 16:08):

Ju-sh has marked this topic as resolved.

view this post on Zulip Gaëtan Gilbert (Dec 21 2021 at 16:08):

https://coq.github.io/doc/master/refman/language/extensions/match.html#second-destructuring-let-syntax


Last updated: Jan 28 2023 at 06:30 UTC