Stream: Coq devs & plugin devs

Topic: inconsistent Hurkens


view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (May 11 2020 at 15:00):

@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).

view this post on Zulip 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 16 2021 at 02:03 UTC