The Coq mailing list

[Nico <nlehmann AT dcc.uchile.cl>]

On Fri, May 15, 2015 at 3:40 PM Gregory Malecha <gmalecha AT cs.harvard.edu> wrote:

Hi, Nico --

I don't believe this is possible. If the type is embedded inside of a term, then that term could be opened up via Ltac, and then Ltac could construct a term using constr and avoid your check.

I don't clearly understand what do you mean here.

 

It is possible to express your restriction via arguments? For example, if you want a type function that requires a type with a decidable equality there are several ways to do it:

I don't think is posible to express the restricion in this way because I need to access the axioms that an argument take as assumptions.