The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

On Sun, Jun 16, 2013 at 3:22 AM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:

> Type does not have decidable equality, and you cannot productively
> destruct/match on a thing of type Type.

That makes sense.

> Additionally, the match you use is
> in Ltac; it matches on a syntactic level, unlike the non-ltac match.

And that, I guess, is why I expected it to work anyway. ;-) A
syntactic match is exactly what I'm after (modulo delta/beta/zeta
reduction). I'm basically trying to create some syntactic sugar. And
isn't syntactic equality decidable?

> You will probably want to reify your types so that you can distinguish
> function types from other types.

Indeed. But I won't need that until I write the recursive definition
later, right? For the moment, I'm trying to solve one problem at a
time: that of matching the 'T' of 'primitive' to the 'T' of
'delta_op'.

> Appologies if this is not enough information; I'm typing from my cellphone
> at the moment and thus being concise.

No problem. Though if you can find some time later, I would appreciate
an example of how to do this properly. It seems like it should be
possible.

Thanks!

--
www.mhelvens.net