Gaëtan Gilbert (May 11 2020 at 14:56): Gaëtan Gilbert (May 11 2020 at 14:56):Seeing through the indirections needed to make Hurkens typecheck can be hard, so I would be interested in having some Inconsistencies.v file where we locally use unsafe flags to prove inconsistencies. That way when someone asks what happens if we get Type in Type we don't need to say "it lets you instantiate the hypotheses of Hurkens.Bla.paradox with such and such", instead we point them to some code like
Unset Universe Checking.
Definition bad := let T := Type in T : T.
Set Universe Checking.
Lemma paradox : False.
Proof. refine (Hurkens.Bla.paradox (*...*)). (*...*) Qed.
@Gaëtan Gilbert I'm unsure this would be suitable for a stdlib library file. However, it is for the documentation, and in fact, a number of such paradox are shown here: https://coq.github.io/doc/master/refman/language/cic.html#correctness-rules (see the three last examples).
Jason Gross (May 12 2020 at 00:34):Yes, this seems like something that should live in coq-contribs/coq-community, or, indeed, just in the refman. Perhaps Hurkens.v could link to that section of the refman?
Last updated: Oct 08 2024 at 14:01 UTC