Julin S (Dec 21 2021 at 15:53): 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 *)
Definition foo '((a,b) : (nat * nat)): nat := a.
Thanks. What does the ' do? Is there a place where I can read more about it?
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
Julin S (Dec 21 2021 at 16:08):Thanks again.
Notification Bot (Dec 21 2021 at 16:08):Ju-sh has marked this topic as resolved.
Gaëtan Gilbert (Dec 21 2021 at 16:08):Last updated: Apr 20 2024 at 09:01 UTC