coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
Archive powered by MhonArc 2.6.16.