The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users/Team,

 

I did some experiments with dependent types again, and I think the thing I am sometimes missing is an opaquify operator. Terms of dependent types usually contain a mixture of “data” expressions one is interested in and “proof” expressions for which just the type is interesting. The idea is that if I have a term, opaquify(term) makes the term as such opaque, only the type remains visible. The term cannot be unified any more, only its type.  When printing an opaquified term, it is printed as something like opaque:<type> or maybe just opaque in case the type can be inferred.

 

I can use notations and to a certain extent opaque proofs to hide the proof parts of terms of dependent type, but sometimes I think it might also help Coq’s performance to know that it should never look into the term as such, just as if it would be an opaque proof term. Another benefit would be less distraction and maybe a better understanding of the users.

 

My question: am I doing something wrong when I end up at this thought? How are others handling this?

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928