Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Consistency of axiom about dynamic packages?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Consistency of axiom about dynamic packages?


chronological Thread 
  • From: "Andrew McCreight" <continuation AT gmail.com>
  • To: "Adam Chlipala" <adamc AT hcoop.net>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Consistency of axiom about dynamic packages?
  • Date: Mon, 9 Jun 2008 15:42:23 -0700
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:in-reply-to:mime-version :content-type:references; b=kwLq0tPSrxX5EiQa8EAyz8A07/3FnWxZwHzDr4uB+halpjP/BVshX3o610LHFTR8EP ldgFzTF42VIdxTxQH6LlKvvVehlqCjjMM1Y1E8/RHi5YYMlfilOQREuuGmOCiMzg9aYS hRS93pVYcs67SYbGDo38n51kQopHKqAkrZwyY=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
I could be wrong, but this looks very similar to a question that was asked a few years ago:

http://coq.inria.fr/mailing-lists/coqclub/200201/msg00001.html

In short, the answer was no.

On Mon, Jun 9, 2008 at 3:37 PM, Adam Chlipala <adamc AT hcoop.net> wrote:
Does anyone know if it would be consistent with (impredicative Set) CIC to assert the injectivity of the [Dyn] constructor below as an axiom?

Inductive dynamic : Set :=
 | Dyn : forall T, T -> dynamic.

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
        http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club


Archive powered by MhonArc 2.6.16.

Top of Page