The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I guess it does not work, but you can still try to do something like: «Notation "'indentity_ind'" := (Coq.Init.True Coq.Init.False).» (or use Abbreviation).
The idea would be to create a notation to an ill-typed term.
As far as I can remember, Coq only checks that all terms inside of a notation are defined, but does not check types at Notation definition.
When 'identity_ind' would be used, it would trigger an error, as it is not well typed.
Note that this works only for terms defined AFTER the notation. And in case of "identity_rect", forbidding it this way would not forbid "identity_rec" which is defined from "identity_rect".

Like Arnaud, I do not really see the point of such a feature.

I guess it covers the case where you define at term with X_{rec,rect,ind} as identifier before defining an inductive called X.
In this case, it was either a bad idea to name it X_{rec,rect,ind} and this should be changed, or you want to replace the induction principle, in which case it is better to deactivate automatic generation of induction principle ("Unset Elimination Scheme." if I remember well) and then define your own.

2014-10-24 14:26 GMT+02:00 Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>:

I don't think there is. What sort of use-case do you have in mind?

On 24 October 2014 12:47, Vladimir Voevodsky <vladimir AT ias.edu> wrote:

Hello,

is there a way to make sure that a certain identifier can not be used? The closest that I know to it is to make an identifier opaque but
I would like to make sure that an identifier is not used at all, e.g., I would like to say

Hide identity_ind.

and then if a tactic wants to use it it will generate an error.

Vladimir.

--
.../Sedrikov\...