The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

On Aug 3, 2014, at 10:51 PM, Gabriel Scherer <gabriel.scherer AT gmail.com> wrote:

Definition nonsense ( x : un ) := match x with y => 0 end .

Is this supposed to make sense?

This makes perfect sense.

Yes, I agree, sorry for raising a vague objection. But the question of what precisely the syntax of a "match" is, to me, remains. What is the arity of "match" in the sense of, e.g., nominal signatures? 

How many arguments it has? How many variables each argument binds? 

Vladimir.

 

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail