The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi all,

I'm working in an axiom-free Coq development, and the elim restriction
is getting in our way. I considered moving parts of our development from
Prop to Type, but Coq's support for that is pretty poor -- in terms of
notation, but (most importantly) in terms of rewriting. The Setoid
mechanism forces the relation to be "A -> A -> Prop".

However (if I recall correctly), the elim restriction is actually only
needed because Coq wants to remain compatible with classical axioms.
Since we try hard to avoid these, it is rather unfortunate that we still
have to pay this prize. Of course we could just assume an axiom
"inhabited T -> T", but that would not reduce properly, and of course it
would mean we are no longer axiom-free. (I'm not sure if the part about
computation would practically matter, but foundationally, it'd be nice
to keep everything computational.)

So I wonder, would it be possible to add a flag to Coq to disable the
elim restriction? Would that make sense? It's a little like
type-in-type, except that it's not actually unsound if not combined with
classical axioms.

Kind regards,
Ralf