coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] UIP + code extraction ?

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

[Coq-Club] UIP + code extraction ?, Vilius Naudziunas