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?
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
Ju-sh has marked this topic as resolved.
Last updated: Jan 28 2023 at 06:30 UTC