Skip to Content.
Sympa Menu

coq-club - [Coq-Club] UIP + code extraction ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] UIP + code extraction ?


chronological Thread 
  • From: Vilius Naudziunas <vn229 AT cam.ac.uk>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] UIP + code extraction ?
  • Date: Tue, 01 Feb 2011 15:01:07 +0000

Dear all,

Does anyone know if assuming Uniqueness of Identity Proofs (Coq.Logic.EqdepFacts)
breaks code extraction from proofs? Is it possible to get a runtime error in extracted
ocaml code during type upcasting?

I add UIP using the following lines:

  Require Import Coq.Logic.EqdepFacts.
  Axiom UIP : forall A, UIP_ A.

It seems that in all examples I tried references to UIP are removed during code extraction,
since it is Prop.

Kind regards

Vilius



Archive powered by MhonArc 2.6.16.

Top of Page