coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] What problem does an extracted function solve?
- Date: Mon, 4 Nov 2013 10:11:54 +0000
- Accept-language: en-GB, en-US
It's easy to show that
T =
fun (x : nat) (H : x > 0) => exist (fun y : nat => y > 0) x H
: forall x : nat, x > 0 -> {y : nat | y > 0}
Clearly, T cannot produce an output unless it is given a nat x and a proof
that x > 0. However, I'm not sure what to make of the function extracted from
T, i.e.
let t x =
x
because t can produce an output for all values of x, not only x > 0. On the
face of it, t appears to solve a different problem than T. How should one
view the relationship between t and T?
Regards,
Jeff.
- [Coq-Club] What problem does an extracted function solve?, Terrell, Jeffrey, 11/04/2013
- Re: [Coq-Club] What problem does an extracted function solve?, Pierre Courtieu, 11/04/2013
- Re: [Coq-Club] What problem does an extracted function solve?, Cedric Auger, 11/04/2013
- Re: [Coq-Club] What problem does an extracted function solve?, Terrell, Jeffrey, 11/04/2013
- Re: [Coq-Club] What problem does an extracted function solve?, Pierre Letouzey, 11/04/2013
- Re: [Coq-Club] What problem does an extracted function solve?, Terrell, Jeffrey, 11/04/2013
- Re: [Coq-Club] What problem does an extracted function solve?, Cedric Auger, 11/04/2013
- Re: [Coq-Club] What problem does an extracted function solve?, Pierre Courtieu, 11/04/2013
Archive powered by MHonArc 2.6.18.