coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Check faulty?

From: Gert Smolka <smolka AT ps.uni-saarland.de>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Check faulty?
Date: Thu, 11 Apr 2013 11:37:50 +0200

I would consider the following a bug of the commands Check and Compute. It
seems to me that they should report that they cannot derive the implicit
instance argument of f (for good reasons). Commands below were run with Coq
8.4pl2 (April 2013).

Set Printing Implicit.
Class F := {f : False}.
Check (f:False).
Compute f.

So far I assumed that after elaboration Check calls the kernel type checker
to confirm its findings. I would be curious to know why this is not the case.

Gert

[Coq-Club] Check faulty?, Gert Smolka, 04/11/2013
- Re: [Coq-Club] Check faulty?, Gert Smolka, 04/22/2013
  - Re: [Coq-Club] Check faulty?, Jason Gross, 04/26/2013
    - Re: [Coq-Club] Check faulty?, Gert Smolka, 04/28/2013